mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CongrExclamation
/-- Conditionally runs a congruence strategy depending on the predicate `b` applied to the config.
 -/
_private.Mathlib.Tactic.CongrExclamation.0.Lean.MVarId.congrPasses!.when : (Congr!.Config → Bool) →
  (Congr!.Config → Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) →
    Congr!.Config → Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_diff_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = false → (m₁.diff m₂).getKey! k = m₁.getKey! k
-- Mathlib.Data.FunLike.Group
/-- Coercion as a multiplicative homomorphism.  -/
FunLike.coeMulHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) → [inst : FunLike F α β] → [inst_1 : Mul F] → [inst_2 : Mul β] → [IsMulApply F α β] → F →ₙ* α → β
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.base.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {ι : C → Type w}
  [inst_1 : SizeOf C] [inst_2 : (a : C) → SizeOf (ι a)] (X : C) (a : ι X),
  sizeOf (CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ X a) = 1 + sizeOf X + sizeOf a
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.coimageIsoImage'_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Abelian.coimageIsoImage' f).hom =
    CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.kernel.ι f) (CategoryTheory.Limits.factorThruImage f) ⋯
-- Mathlib.RingTheory.Perfection
PreTilt.instCharP : ∀ (O : Type u₂) [inst : CommRing O] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p],
  CharP (PreTilt O p) p
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.lift_tmul : ∀ {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] (f : A →ₐ[R] C)
  (g : B →ₐ[R] C)
  (h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)) (a : A)
  (b : B), (GradedTensorProduct.lift 𝒜 ℬ f g h_anti_commutes) (a ᵍ⊗ₜ[R] b) = f a * g b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Complex.sin` is complex analytic.  -/
Complex.analyticWithinAt_sin : ∀ {x : ℂ} {s : Set ℂ}, AnalyticWithinAt ℂ Complex.sin s x
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_ne_top : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.einfsep ≠ ⊤ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y ≠ ⊤
-- Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization
Submonoid.LocalizationMap.uniqueFactorizationMonoid : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoidWithZero M] [inst_1 : CommMonoidWithZero N] {S : Submonoid M}
  (f : S.LocalizationMap N) [UniqueFactorizationMonoid M], UniqueFactorizationMonoid N
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.coe_copy : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (f : A →⋆ₐ[R] B) (f' : A → B)
  (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The type underlying the homotopy category of a 2-truncated simplicial set `V`.  -/
SSet.Truncated.HomotopyCategory : SSet.Truncated 2 → Type u
-- Batteries.Data.List.Lemmas
List.countPBefore_cons_succ_of_neg : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {i : ℕ} {a : α},
  p a = false → List.countPBefore p (a :: xs) (i + 1) = List.countPBefore p xs i
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.comp.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (hnp : N →ₙ+ P)
  (hmn : M →ₙ+ N), hnp.comp hmn = { toFun := fun x => hnp (hmn x), map_add' := ⋯ }
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists'.toList.match_1.eq_2 : ∀ {α : Type u_1} (motive : (x : Bool) → Lists' α x → Sort u_2) (h_1 : (a : α) → motive false (Lists'.atom a))
  (h_2 : Unit → motive true Lists'.nil)
  (h_3 : (b : Bool) → (a : Lists' α b) → (l : Lists' α true) → motive true (a.cons' l)),
  (match true, Lists'.nil with
    | .(false), Lists'.atom a => h_1 a
    | .(true), Lists'.nil => h_2 ()
    | .(true), a.cons' l => h_3 b a l) =
    h_2 ()
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.instNeBotConditionalOfNonemptyOfIsDirectedOrderOfIsCodirectedOrder : ∀ (β : Type u_2) [inst : Preorder β] [inst_1 : LocallyFiniteOrder β] [Nonempty β] [IsDirectedOrder β]
  [IsCodirectedOrder β], (SummationFilter.conditional β).NeBot
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.isAffineHom_diagonal_iff : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.IsAffineHom (CategoryTheory.Limits.pullback.diagonal f) ↔
    ∀ (U : Y.Opens),
      AlgebraicGeometry.IsAffineOpen U →
        ∀ V₁ ≤ (TopologicalSpace.Opens.map f.base).obj U,
          ∀ V₂ ≤ (TopologicalSpace.Opens.map f.base).obj U,
            AlgebraicGeometry.IsAffineOpen V₁ →
              AlgebraicGeometry.IsAffineOpen V₂ → AlgebraicGeometry.IsAffineOpen (V₁ ⊓ V₂)
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalRefine' : Lean.Elab.Tactic.Tactic
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestRevMatch_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos ↔
    String.Slice.Pattern.Model.IsRevMatch pat pos ∧ ∀ pos' < pos, ¬String.Slice.Pattern.Model.IsRevMatch pat pos'
-- Mathlib.RingTheory.PowerBasis
PowerBasis.minpolyGen_eq : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] (pb : PowerBasis A S),
  pb.minpolyGen = minpoly A pb.gen
-- Mathlib.Order.Heyting.Basic
/-- Construct a Heyting algebra from the lattice structure and complement operator alone.  -/
HeytingAlgebra.ofCompl : {α : Type u_2} →
  [inst : DistribLattice α] →
    [BoundedOrder α] → (compl : α → α) → (∀ (a b c : α), a ≤ compl b ⊔ c ↔ a ⊓ b ≤ c) → HeytingAlgebra α
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.value : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu → Lean.Compiler.LCNF.Code pu
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.replaceLPsWithVars : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddCommMonoid : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [AddCommMonoid M] → AddCommMonoid (l.Germ M)
-- Mathlib.Algebra.DirectSum.Basic
_private.Mathlib.Algebra.DirectSum.Basic.0.DFinsupp.extendWith.match_1.splitter : {ι : Type u_1} →
  (motive : Option ι → Sort u_2) → (i : Option ι) → (Unit → motive none) → ((val : ι) → motive (some val)) → motive i
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaEquiv_yoneda_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.yonedaEquiv (CategoryTheory.yoneda.map f) = f
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- A structured arrow is called universal if it is initial.  -/
CategoryTheory.StructuredArrow.IsUniversal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} → {T : CategoryTheory.Functor C D} → CategoryTheory.StructuredArrow S T → Type (max (max u₁ v₂) v₁)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- A version of `WithBot.map` for `AddHom`s.  -/
AddHom.withBotMap : {M : Type u_1} → {N : Type u_2} → [inst : Add M] → [inst_1 : Add N] → (M →ₙ+ N) → WithBot M →ₙ+ WithBot N
-- Mathlib.RingTheory.Coalgebra.Quotient
Submodule.IsCoideal.counit_eq_zero : ∀ {R : Type u_1} {C : Type u_2} {inst : CommRing R} {inst_1 : AddCommGroup C} {inst_2 : Module R C}
  {inst_3 : CoalgebraStruct R C} {I : Submodule R C} [self : I.IsCoideal] ⦃x : C⦄, x ∈ I → CoalgebraStruct.counit x = 0
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNonUnitalSemiring : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalSemiring R] → [IsTopologicalSemiring R] → NonUnitalSemiring (SeparationQuotient R)
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.pointwise_smul_le_iff₀ : ∀ {M : Type u_1} {R : Type u_2} [inst : GroupWithZero M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M},
  a ≠ 0 → ∀ {S T : Subsemiring R}, a • S ≤ T ↔ S ≤ a⁻¹ • T
-- Mathlib.Data.Num.Bitwise
/-- `a.testBit n` is `true` iff the `n`-th bit (starting from the LSB) in the binary representation
of `a` is active. If the size of `a` is less than `n`, this evaluates to `false`.  -/
PosNum.testBit : PosNum → ℕ → Bool
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_self_const_mul' : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] (u : Rˣ) (f : α → R) (l : Filter α),
  Asymptotics.IsBigOWith ‖↑u⁻¹‖ l f fun x => ↑u * f x
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β] {f g : SupBotHom α β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
/-- Scalar multiple of a continuous linear equivalence (given certain properties are satisfied).  -/
_private.Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv.0.auxContinuousLinearEquiv : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            [inst_3 : CompleteSpace V] →
              [inst_4 : NormedAddCommGroup W] →
                [inst_5 : InnerProductSpace 𝕜 W] →
                  [inst_6 : CompleteSpace W] →
                    (e : V ≃L[𝕜] W) →
                      {α α' : 𝕜} →
                        α ≠ 0 →
                          α' * α' = α⁻¹ →
                            ContinuousLinearMap.adjoint ↑e ∘SL ↑e = α • ContinuousLinearMap.id 𝕜 V →
                              ↑e ∘SL ContinuousLinearMap.adjoint ↑e = α • ContinuousLinearMap.id 𝕜 W → V ≃L[𝕜] W
-- Mathlib.Data.Nat.Init
/-- Given a predicate on two naturals `P : ℕ → ℕ → Prop`, `P a b` is true for all `a < b` if
`P (a + 1) (a + 1)` is true for all `a`, `P 0 (b + 1)` is true for all `b` and for all
`a < b`, `P (a + 1) b` is true and `P a (b + 1)` is true implies `P (a + 1) (b + 1)` is true.  -/
Nat.diag_induction : ∀ (P : ℕ → ℕ → Prop),
  (∀ (a : ℕ), P (a + 1) (a + 1)) →
    (∀ (b : ℕ), P 0 (b + 1)) →
      (∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)) → ∀ (a b : ℕ), a < b → P a b
-- Mathlib.CategoryTheory.Galois.Basic
/-- A `PreGaloisCategory` is a `GaloisCategory` if it admits a fiber functor.  -/
CategoryTheory.GaloisCategory : (C : Type u₁) → [CategoryTheory.Category.{u₂, u₁} C] → Prop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_insertIfNew_le : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, (m.insertIfNew k v).size ≤ m.size + 1
-- Mathlib.GroupTheory.Abelianization.Finite
instFintypeAbelianizationOfDecidablePredMemSubgroupCommutator : {G : Type u_1} → [inst : Group G] → [Fintype G] → [DecidablePred fun x => x ∈ commutator G] → Fintype (Abelianization G)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionIdentifier.const.inj : ∀ {declName declName_1 : Lean.Name},
  Lean.Lsp.CompletionIdentifier.const declName = Lean.Lsp.CompletionIdentifier.const declName_1 → declName = declName_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (Std.ExtDHashMap.ofList l).getKeyD k' fallback = k
-- Mathlib.Geometry.Convex.Cone.Basic
/-- **Alias** of `ConvexCone.IsReproducing.span_eq_top`. -/
ConvexCone.IsReproducing.isGenerating : ∀ {R : Type u_7} {M : Type u_8} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {C : ConvexCone R M}, C.IsReproducing → Submodule.span R ↑C = ⊤
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.uniqueHomToTrivial.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.AddGrp C),
  A.uniqueHomToTrivial =
    (have this := CategoryTheory.InducedCategory.homEquiv;
      this).unique
-- Mathlib.Algebra.Algebra.Hom.Rat
RingEquiv.toAlgHom_toRatAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (f : R ≃+* S), ↑f.toRatAlgEquiv = (↑f).toRatAlgHom
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.isUniformInducing_postcomp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : UniformSpace F]
  [inst_7 : IsUniformAddGroup F] {G : Type u_5} [inst_8 : AddCommGroup G] [inst_9 : UniformSpace G]
  [inst_10 : IsUniformAddGroup G] [inst_11 : Module 𝕜 G] (g : F →L[𝕜] G),
  IsUniformInducing ⇑g → IsUniformInducing g.compContinuousMultilinearMap
-- Init.Control.Lawful.Instances
OptionT.run_failure : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m], failure.run = pure none
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier : Lean.FromJson Lean.Lsp.VersionedTextDocumentIdentifier
-- Init.Dynamic
/-- Creates a `TypeName` instance.

For safety, it is required that the constant `typeName` is definitionally equal
to `α`.
 -/
TypeName.mk : (α : Type u) → Lean.Name → TypeName α
-- Mathlib.CategoryTheory.Simple
CategoryTheory.Simple.of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  [CategoryTheory.Simple Y] (i : X ≅ Y), CategoryTheory.Simple X
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Circle integrability is invariant when functions change along discrete sets.  -/
circleIntegrable_congr_codiscreteWithin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E},
  f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂ → (CircleIntegrable f₁ c R ↔ CircleIntegrable f₂ c R)
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitHomIsoLimitYoneda_inv_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor I C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda F A).inv
      (TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F i) g) =
    CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj A)) (Opposite.op i)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      ∀ {f g : 𝕜 → F},
        ContDiffWithinAt 𝕜 (↑n) f s x →
          ContDiffWithinAt 𝕜 (↑n) g s x →
            iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.dirichletInverseFun_apply_zero : ∀ {R : Type u_1} [inst : Ring R] (f : ℕ → R) (hf : Invertible (f 1)), ArithmeticFunction.dirichletInverseFun f hf 0 = 0
-- Init.Grind.AC
Lean.Grind.AC.norm_a : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} (e : Lean.Grind.AC.Expr)
  (s : Lean.Grind.AC.Seq), e.toSeq.beq' s = true → Lean.Grind.AC.Expr.denote ctx e = Lean.Grind.AC.Seq.denote ctx s
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.instSupSet : (R : Type u_1) → [inst : NonUnitalNonAssocRing R] → SupSet (TwoSidedIdeal R)
-- Init.Data.Vector.Lemmas
Vector.getElem?_replicate : ∀ {α : Type u_1} {a : α} {n i : ℕ}, (Vector.replicate n a)[i]? = if i < n then some a else none
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `QuadraticForm.toMatrix'_smul`. -/
QuadraticForm.QuadraticMap.toMatrix'_smul : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  (a : R) (Q : QuadraticForm R (n → R)), (a • Q).toMatrix' = a • Q.toMatrix'
-- Mathlib.Analysis.Convex.Segment
Pi.openSegment_subset : ∀ {𝕜 : Type u_1} {ι : Type u_5} {M : ι → Type u_6} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module 𝕜 (M i)] {s : Set ι} (x y : (i : ι) → M i),
  openSegment 𝕜 x y ⊆ s.pi fun i => openSegment 𝕜 (x i) (y i)
-- Std.Http.Protocol.H1
/-- Checks whether the initial framing mode already exceeds `maxBodySize` before any
body bytes are read.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.exceedsBodyLimitForMode : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine.BodyMode✝ → Bool
-- Mathlib.Algebra.Star.Module
IsSelfAdjoint.skewAdjointPart_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] {x : A}, IsSelfAdjoint x → (skewAdjointPart R) x = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α} {v : β k}, (↑(m.insertIfNew k v)).isEmpty = false
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instMulAction : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module S F] →
                      {M : Type u_7} →
                        [inst_6 : Monoid M] →
                          [inst_7 : DistribMulAction M F] → [SMulCommClass S M F] → MulAction M (E →ₛₗ.[σ] F)
-- Mathlib.Data.Seq.Computation
Computation.has_map_eq_map : ∀ {α β : Type u} (f : α → β) (c : Computation α), f <$> c = Computation.map f c
-- Init.Data.Option.Lemmas
Option.merge_beq_none : ∀ {α : Type u_1} [inst : BEq α] {o o' : Option α} {f : α → α → α},
  (Option.merge f o o' == none) = (o == none && o' == none)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- **Alias** of `dimH_coe_finset`. -/
Finset.dimH_zero : ∀ {X : Type u_2} [inst : EMetricSpace X] (s : Finset X), dimH ↑s = 0
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
inl_coprodIsoPushout_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y))
      (coprodIsoPushout X Y).inv =
    CategoryTheory.Limits.coprod.inl
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.coe_prodComm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] (I : ModelWithCorners 𝕜 E H)
  (J : ModelWithCorners 𝕜 F G) (M : Type u_9) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] (N : Type u_11)
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] (n : WithTop ℕ∞),
  ⇑(Diffeomorph.prodComm I J M N n) = Prod.swap
-- Aesop.Tree.Free
_private.Aesop.Tree.Free.0.Aesop.mkDummyRefs : BaseIO (Aesop.GoalRef × Aesop.MVarClusterRef)
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.iff_mulOpposite : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G} {a0 b0 : G},
  UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } A)
      (MulOpposite.op b0) (MulOpposite.op a0) ↔
    UniqueMul A B a0 b0
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.pderiv_X : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (i j : σ),
  (MvPowerSeries.pderiv R i) (MvPowerSeries.X j) = Pi.single i 1 j
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.instMonoidalCategory.tensorObj_form : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] (X Y : QuadraticModuleCat R),
  (QuadraticModuleCat.instMonoidalCategory.tensorObj X Y).form = X.form.tmul Y.form
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closed thickening `Metric.cthickening δ₁ E` is contained in the open thickening
`Metric.thickening δ₂ E` if the radius of the latter is positive and larger.  -/
Metric.cthickening_subset_thickening' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ₁ δ₂ : ℝ},
  0 < δ₂ → δ₁ < δ₂ → ∀ (E : Set α), Metric.cthickening δ₁ E ⊆ Metric.thickening δ₂ E
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_p₁ : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (x x_1 : data.I₀)
  (j : data.I₁ x x_1), data.toPreOneHypercover.p₁ j = F.map (data.p₁ j)
-- Mathlib.RingTheory.Valuation.ValuationRing
isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective : ∀ {𝒪 : Type u} {K : Type v} [inst : CommRing 𝒪] [inst_1 : Field K] [inst_2 : Algebra 𝒪 K],
  (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) →
    Function.Injective ⇑(algebraMap 𝒪 K) → IsFractionRing 𝒪 K
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.flag_le_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (b : Module.Basis (Fin n) R M) {k : Fin (n + 1)} {p : Submodule R M},
  b.flag k ≤ p ↔ ∀ (i : Fin n), i.castSucc < k → b i ∈ p
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_const_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f : 𝕜 → F},
  0 < n → ∀ (c : F), iteratedDeriv n (fun z => c - f z) x = iteratedDeriv n (-f) x