mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Category.Bipointed
bipointedToPointedSnd_comp_forget : bipointedToPointedSnd.comp (CategoryTheory.forget Pointed) = CategoryTheory.forget Bipointed
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.comp_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Polynomial R)
  (x : PolynomialModule R M),
  (PolynomialModule.comp p) x =
    (PolynomialModule.eval p) ((PolynomialModule.map (Polynomial R) (PolynomialModule.lsingle R 0)) x)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIocDiv hp a (b + m • p) = toIocDiv hp a b + m
-- Mathlib.Algebra.Order.Ring.Abs
Int.le_abs_of_dvd : ∀ {a b : ℤ}, b ≠ 0 → a ∣ b → a ≤ |b|
-- Mathlib.Computability.Primrec.Basic
Primcodable.mem_range_encode : ∀ {α : Type u_1} [inst : Primcodable α], PrimrecPred fun n => n ∈ Set.range Encodable.encode
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ioc_inl_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (a : α) (b : β),
  Finset.Ioc (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ioi a).disjSum (Finset.Iic b))
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_union : ∀ {X : Type u_2} [inst : EMetricSpace X] (s t : Set X), dimH (s ∪ t) = max (dimH s) (dimH t)
-- Init.Data.String.TakeDrop
/-- Advances `pos` as long as `pat` matches.
 -/
String.Pos.skipWhile : {ρ : Type} → {s : String} → s.Pos → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → s.Pos
-- Mathlib.Algebra.GroupWithZero.Nat
Nat.instMulZeroClass : MulZeroClass ℕ
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.smul_iso_hom_eq_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : (CategoryTheory.CatCenter C)ˣ) {X Y : C} (f : X ≅ Y)
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (z • f).hom h =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp ((↑z).app Y) h)
-- Mathlib.RingTheory.Nakayama
/-- [Stacks Tag 00DV](https://stacks.math.columbia.edu/tag/00DV) ((3) see `Submodule.localized₀_le_localized₀_of_smul_le` for the second conclusion.) -/
Submodule.exists_sub_one_mem_and_smul_le_of_fg_of_le_sup : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {N N' P : Submodule R M}, N'.FG → N' ≤ P → P ≤ N ⊔ I • N' → ∃ r, r - 1 ∈ I ∧ r • P ≤ N
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportErrorData.new : BaseIO Lean.Meta.RefinedDiscrTree.ImportErrorData✝
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend_iUnion_nat : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal}
  (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)) {f : ℕ → Set α} (hm : ∀ (i : ℕ), P (f i)),
  m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯ → MeasureTheory.extend m (⋃ i, f i) = ∑' (i : ℕ), MeasureTheory.extend m (f i)
-- Mathlib.Data.Bundle
Bundle.instInhabitedTotalSpaceOfDefault : {B : Type u_1} →
  {F : Type u_2} →
    (E : B → Type u_3) → [inst : Inhabited B] → [Inhabited (E default)] → Inhabited (Bundle.TotalSpace F E)
-- Init.Data.Repr
instReprUnit : Repr Unit
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_subset_ge_of_subset_image : ∀ {α β : Type u} (f : α → β) {s : Set α} {t : Set β}, t ⊆ f '' s → Cardinal.mk ↑t ≤ Cardinal.mk ↑{x | x ∈ s ∧ f x ∈ t}
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.num_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsDomain R] {I : FractionalIdeal (nonZeroDivisors R) K}, I.num = 0 ↔ I = 0
-- Mathlib.RingTheory.KrullDimension.Basic
Ideal.isMaximal_of_isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] (I : Ideal R) [I.IsPrime], I.IsMaximal
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.glue!.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (r : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (r : Std.DTreeMap.Internal.Impl α β) →
      (sz' : ℕ) →
        (k' : α) →
          (v' : β k') →
            (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
              r = Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'' →
                motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r''))
  (sz' : ℕ) (k' : α) (v' : β k') (l'' r'' : Std.DTreeMap.Internal.Impl α β),
  r = Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'' →
    (match r with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | r@h:(Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') => h_2 r sz' k' v' l'' r'' h) ≍
      h_2 (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') sz' k' v' l'' r'' ⋯
-- Mathlib.Order.Category.BoolAlg
BoolAlg.dual_map : ∀ {X Y : BoolAlg} (f : X ⟶ Y), BoolAlg.dual.map f = BoolAlg.ofHom (BoundedLatticeHom.dual (BoolAlg.Hom.hom f))
-- Init.System.FilePath
System.FilePath.instHDivString : HDiv System.FilePath String System.FilePath
-- Init.Classical
Classical.strongIndefiniteDescription : {α : Sort u} → (p : α → Prop) → Nonempty α → { x // (∃ y, p y) → p x }
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.comap_comap : ∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph X} (f : V → W) (g : W → X),
  SimpleGraph.comap f (SimpleGraph.comap g G) = SimpleGraph.comap (g ∘ f) G
-- Mathlib.Analysis.Calculus.Deriv.Inverse
HasDerivWithinAt.eventually_ne : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {s : Set 𝕜} {x : 𝕜} {c : F},
  HasDerivWithinAt f f' s x → f' ≠ 0 → ∀ᶠ (z : 𝕜) in nhdsWithin x (s \ {x}), f z ≠ c
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- Change of variable formula for differentiable functions (one-variable version): if a function
`f` is injective and differentiable on a measurable set `s ⊆ ℝ`, then the Bochner integral of a
function `g : ℝ → F` on `f '' s` coincides with the integral of `|(f' x)| • g ∘ f` on `s`.  -/
MeasureTheory.integral_image_eq_integral_abs_deriv_smul : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      Set.InjOn f s → ∀ (g : ℝ → F), ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, |f' x| • g (f x)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.ext_iff : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] {f g : ContinuousMapZero X R}, f = g ↔ ∀ (x : X), f x = g x
-- Mathlib.Order.Interval.Set.Image
StrictAntiOn.image_Ioo_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  StrictAntiOn f (Set.Icc a b) → f '' Set.Ioo a b ⊆ Set.Ioo (f b) (f a)
-- Init.Data.List.Control
List.mapM.loop : {m : Type u → Type v} → [Monad m] → {α : Type w} → {β : Type u} → (α → m β) → List α → List β → m (List β)
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.mulInitial_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X (⊥_ C)],
  (CategoryTheory.Limits.mulInitial X).inv = CategoryTheory.Limits.initial.to (X ⨯ ⊥_ C)
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.IsMaxRank.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ),
  NumberField.Units.IsMaxRank u = LinearIndependent ℝ fun i => (NumberField.Units.logEmbedding K) (Additive.ofMul (u i))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∈ t₂ → (t₁ \ t₂).getD k fallback = fallback
-- Lean.Elab.MutualInductive
/-- Function to collect additional level metavariables that are header-like (e.g. in `extends` clauses in `structure`).
Header-like level metavariables can be promoted to be level parameters.  -/
Lean.Elab.Command.InductiveElabStep2.collectExtraHeaderLMVars : Lean.Elab.Command.InductiveElabStep2 → StateRefT' IO.RealWorld Lean.CollectLevelMVars.State Lean.MetaM Unit
-- Mathlib.Algebra.CubicDiscriminant
Cubic.ne_zero_of_d_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.d ≠ 0 → P.toPoly ≠ 0
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.lt_irrefl : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f : CauSeq α abs}, ¬f < f
-- Mathlib.RingTheory.Ideal.Maps
Module.mem_annihilator_iff_lsmul_eq_zero : ∀ {M : Type u_2} [inst : AddCommMonoid M] {R : Type u_4} [inst_1 : CommSemiring R] [inst_2 : Module R M] {r : R},
  r ∈ Module.annihilator R M ↔ (LinearMap.lsmul R M) r = 0
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.SimpleFunc.lintegral_eq_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} (f : MeasureTheory.SimpleFunc α ENNReal) (μ : MeasureTheory.Measure α),
  ∫⁻ (a : α), f a ∂μ = f.lintegral μ
-- Std.Http.Data.Response
/-- The content of the response.
 -/
Std.Http.Response.body : {t : Type} → Std.Http.Response t → t
-- Std.Data.DTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the key-value pair with the smallest key.
 -/
Std.DTreeMap.Const.minEntry : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → (t : Std.DTreeMap α (fun x => β) cmp) → t.isEmpty = false → α × β
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opProdIsoCoprod_inv_inl_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv.unop
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl.unop h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
-- Mathlib.Probability.CDF
/-- The cdf tends to 0 at -∞.  -/
ProbabilityTheory.tendsto_cdf_atBot : ∀ (μ : MeasureTheory.Measure ℝ), Filter.Tendsto (↑(ProbabilityTheory.cdf μ)) Filter.atBot (nhds 0)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.var.sizeOf_spec : ∀ (a : Lean.FVarId), sizeOf (Lean.Meta.Match.Example.var a) = 1 + sizeOf a
-- Init.Data.Sum.Lemmas
Sum.Lex.mono_left : ∀ {α : Type u_1} {r₁ r₂ : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {x y : α ⊕ β},
  (∀ (a b : α), r₁ a b → r₂ a b) → Sum.Lex r₁ s x y → Sum.Lex r₂ s x y
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.decompEquiv_symm_contLinear : ∀ (R : Type u_1) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace Q]
  [inst_10 : IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)),
  ((ContinuousAffineMap.decompEquiv R V Q).symm p).contLinear = p.2
-- Mathlib.Order.GaloisConnection.Defs
/-- If `(l, u)` is a Galois connection, then the relation `x ≤ u (l y)` is a transitive relation.
If `l` is a closure operator (`Submodule.span`, `Subgroup.closure`, ...) and `u` is the coercion to
`Set`, this reads as "if `U` is in the closure of `V` and `V` is in the closure of `W` then `U` is
in the closure of `W`".  -/
GaloisConnection.le_u_l_trans : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {x y z : α}, x ≤ u (l y) → y ≤ u (l z) → x ≤ u (l z)
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight_mop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : C} (f : c ⟶ c') (d : D),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f.mop =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d
-- Mathlib.MeasureTheory.Group.ModularCharacter
/-- Independence of modularCharacterFun from the chosen Haar measure.  -/
MeasureTheory.Measure.modularCharacterFun_eq_haarScalarFactor : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : LocallyCompactSpace G] [inst_4 : MeasurableSpace G] [inst_5 : BorelSpace G] (μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] (g : G),
  MeasureTheory.Measure.modularCharacterFun g = (MeasureTheory.Measure.map (fun x => x * g) μ).haarScalarFactor μ
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
TopCat.Sheaf.isIso_iff_isIso_basis : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} {ι : Type u_1} {B : ι → TopologicalSpace.Opens ↑X}
  {F G : TopCat.Sheaf C X},
  TopologicalSpace.Opens.IsBasis (Set.range B) →
    ∀ {φ : F ⟶ G}, (∀ (i : ι), CategoryTheory.IsIso (φ.hom.app (Opposite.op (B i)))) → CategoryTheory.IsIso φ
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.one_mul.sizeOf_spec : ∀ {R : Type u} [inst : Rack R] [inst_1 : SizeOf R] (a : Rack.PreEnvelGroup R),
  sizeOf (Rack.PreEnvelGroupRel'.one_mul a) = 1 + sizeOf a
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenter_compl : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  s.excenter signsᶜ = s.excenter signs
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.takeWhile_eq_filter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {bound : α} {l : List ((a : α) × β a)}
  {l_ordered : List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l},
  List.takeWhile (fun e => (compare e.fst bound).isLE) l = List.filter (fun e => (compare e.fst bound).isLE) l
-- Mathlib.CategoryTheory.Localization.Predicate
/-- The functor of equivalence of localized categories given by `Localization.uniq` is
compatible with the localization functors.  -/
CategoryTheory.Localization.compUniqFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D₁ : Type u_4} →
      {D₂ : Type u_5} →
        [inst_1 : CategoryTheory.Category.{v_4, u_4} D₁] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} D₂] →
            (L₁ : CategoryTheory.Functor C D₁) →
              (L₂ : CategoryTheory.Functor C D₂) →
                (W' : CategoryTheory.MorphismProperty C) →
                  [inst_3 : L₁.IsLocalization W'] →
                    [inst_4 : L₂.IsLocalization W'] → L₁.comp (CategoryTheory.Localization.uniq L₁ L₂ W').functor ≅ L₂
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.continuousAt_inv_infDist_pt : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α},
  x ∉ closure s → ContinuousAt (fun x => (Metric.infDist x s)⁻¹) x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α} {fallback : β},
      (List.map Prod.fst l).contains k = false → (t.insertMany l).getD k fallback = t.getD k fallback
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvectorUnitary.congr_simp : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {n : Type u_4} [inst_1 : Fintype n] {A A_1 : Matrix n n 𝕜} (e_A : A = A_1)
  [inst_2 : DecidableEq n] (hA : A.IsHermitian), hA.eigenvectorUnitary = ⋯.eigenvectorUnitary
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
/-- The manifold derivative of `extChartAt` at the basepoint is the identity.  -/
mfderiv_extChartAt_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I 1 M] {x : M},
  mfderiv% ↑(extChartAt I x) x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LVal.fieldName.inj : ∀ {ref : Lean.Syntax} {name : String} {levels : List Lean.Level} {suffix? : Option Lean.Name}
  {fullRef ref_1 : Lean.Syntax} {name_1 : String} {levels_1 : List Lean.Level} {suffix?_1 : Option Lean.Name}
  {fullRef_1 : Lean.Syntax},
  Lean.Elab.Term.LVal.fieldName ref name levels suffix? fullRef =
      Lean.Elab.Term.LVal.fieldName ref_1 name_1 levels_1 suffix?_1 fullRef_1 →
    ref = ref_1 ∧ name = name_1 ∧ levels = levels_1 ∧ suffix? = suffix?_1 ∧ fullRef = fullRef_1
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
/-- Simp lemmas for rewriting a 2-morphism into a normal form.
 -/
Mathlib.Tactic.BicategoryCoherence.whisker_simps : Lean.ParserDescr
-- Mathlib.Order.Interval.Finset.Box
Finset.disjoint_box_succ_prod : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : LocallyFiniteOrder α]
  [inst_4 : DecidableEq α] (n : ℕ), Disjoint (Finset.box (n + 1)) (Finset.Icc (-↑n) ↑n)
-- Mathlib.Order.Filter.CountableInter
eventually_finset_ball : ∀ {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Finset ι} {p : α → (i : ι) → i ∈ S → Prop},
  (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi
-- Mathlib.LinearAlgebra.Finsupp.Defs
Module.subsingletonEquiv_apply : ∀ (R : Type u_4) (M : Type u_5) (ι : Type u_6) [inst : Semiring R] [inst_1 : Subsingleton R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (x : M), (Module.subsingletonEquiv R M ι) x = 0
-- Mathlib.Util.AddRelatedDecl
/-- Extension of `linter.tacticCheckInstances` to lemmas produced by Mathlib attributes such as
`@[simps]`, `@[reassoc]`, and `@[elementwise]`. Call sites pass the syntax of the user's
attribute (`ref`), the name of the generated lemma (`declName`), and the lemma's type
(`declType`); a warning is emitted at `ref` if `declType` is type-correct at `.default` but
not at `.implicit`, listing the semireducible definitions that would need to be
marked `@[implicit_reducible]` to fix the mismatch.

The check is gated by the existing core option `linter.tacticCheckInstances` and is silent
otherwise; following the convention of the core linter, it does *not* participate in
`linter.all`.  -/
Mathlib.Tactic.warnIfImplicitIllTyped : Lean.Syntax → Lean.Name → Lean.Expr → Lean.MetaM Unit
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Y : CategoryTheory.Over X) {Z : C} (h : Y.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.fst Y.hom (CategoryTheory.CategoryStruct.id X)) h) =
    h
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.adjoin_mem_finset : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Algebra.EssFiniteType R S], Algebra.adjoin R {x | ↑x ∈ Algebra.EssFiniteType.finset R S} = ⊤
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instSurjectiveOfNonemptyOfSubsingletonCarrierCarrierCommRingCat : ∀ {X Y : AlgebraicGeometry.Scheme} [Nonempty ↥X] [Subsingleton ↥Y] (f : X ⟶ Y), AlgebraicGeometry.Surjective f
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- **Chinese remainder theorem**, specialized to two ideals.  -/
Ideal.quotientInfEquivQuotientProd : {R : Type u_2} → [inst : CommRing R] → (I J : Ideal R) → IsCoprime I J → R ⧸ I ⊓ J ≃+* (R ⧸ I) × R ⧸ J
-- Init.Data.UInt.Lemmas
UInt64.mul_def : ∀ (a b : UInt64), a * b = { toBitVec := a.toBitVec * b.toBitVec }
-- Init.PropLemmas
exists_comm : ∀ {α : Sort u_2} {β : Sort u_1} {p : α → β → Prop}, (∃ a b, p a b) ↔ ∃ b a, p a b
-- Init.Data.List.Basic
List.instDecidablePairwise : {α : Type u} → {R : α → α → Prop} → [DecidableRel R] → (l : List α) → Decidable (List.Pairwise R l)
-- Mathlib.SetTheory.Cardinal.Arithmetic
/-- If `α` and `β` are infinite types, then the cardinality of `α × β` is the maximum
of the cardinalities of `α` and `β`.  -/
Cardinal.mul_eq_max : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → Cardinal.aleph0 ≤ b → a * b = max a b
-- Mathlib.Algebra.Group.Units.Basic
Units.val_inv_inj : ∀ {α : Type u} [inst : Monoid α] {u₁ u₂ : αˣ}, ↑u₁⁻¹ = ↑u₂⁻¹ ↔ ↑u₁ = ↑u₂
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
/-- When two morphisms `X ⟶ Y` with `X` cofibrant are related by a left homotopy,
this is a choice of a right homotopy relative to any good path object for `Y`.  -/
HomotopicalAlgebra.LeftHomotopyRel.rightHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          [HomotopicalAlgebra.IsCofibrant X] →
            HomotopicalAlgebra.LeftHomotopyRel f g →
              (Q : HomotopicalAlgebra.PathObject Y) → [Q.IsGood] → Q.RightHomotopy f g
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_comp : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : PerfectRing M p]
  [inst_6 : IsPRadical i p] [inst_7 : ExpChar L p], (PerfectRing.lift i j p).comp i = j
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.length_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp], t.WF → t.toList.length = t.size
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.IsKInjective.homotopyZero_def : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) (hK : HomologicalComplex.Acyclic K) [inst_2 : L.IsKInjective],
  CochainComplex.IsKInjective.homotopyZero f hK = ⋯.some
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLT_iff_isChain`. -/
List.SortedLT.isChain : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLT → List.IsChain (fun x1 x2 => x1 < x2) l
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.Hom.snd : {J : CategoryTheory.Limits.MulticospanShape} →
  (b : J.R) →
    (CategoryTheory.Limits.WalkingMulticospan.left (J.snd b)).Hom (CategoryTheory.Limits.WalkingMulticospan.right b)