mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiable.comp_mdifferentiableOn : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} {s : Set M} {g : M' → M''}, MDiff g → MDiff[s] f → MDiff[s] (g ∘ f)
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.Arrow.hasLiftingProperty_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y),
  CategoryTheory.HasLiftingProperty i p ↔
    ∀ (φ : CategoryTheory.Arrow.mk i ⟶ CategoryTheory.Arrow.mk p), Nonempty (CategoryTheory.Arrow.LiftStruct φ)
-- Lean.DocString.DeferredCheck
/-- The docstring that a deferred check was recorded in. Identifies the docstring without a source
position, so that editing unrelated text doesn't change the public information of the module.
 -/
Lean.Doc.DeferredCheckSite : Type
-- Mathlib.Topology.ContinuousMap.Algebra
/-- If an infinite sum of functions in `C(α, β)` converges to `g` (for the compact-open topology),
then the pointwise sum converges to `g x` for all `x ∈ α`.  -/
ContinuousMap.hasSum_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_3}
  [inst_2 : AddCommMonoid β] [inst_3 : ContinuousAdd β] {f : γ → C(α, β)} {g : C(α, β)} {L : SummationFilter γ},
  HasSum f g L → ∀ (x : α), HasSum (fun i => (f i) x) (g x) L
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.mkₐ_eq_aeval : ∀ {A : Type u_3} {σ : Type u_4} [inst : CommRing A] (I : Ideal (MvPolynomial σ A)),
  Ideal.Quotient.mkₐ A I = MvPolynomial.aeval fun d => (Ideal.Quotient.mk I) (MvPolynomial.X d)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.norm.eq_def : ∀ (p : Int.Internal.Linear.Poly),
  p.norm =
    match p with
    | Int.Internal.Linear.Poly.num k => Int.Internal.Linear.Poly.num k
    | Int.Internal.Linear.Poly.add k v p => Int.Internal.Linear.Poly.insert k v p.norm
-- Init.Data.Option.Lemmas
Option.merge_max : ∀ {α : Type u_1} [inst : Max α], Option.merge max = max
-- Mathlib.Algebra.Homology.Single
ChainComplex.single₀ObjXSelf : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (X : V),
  HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X =
    CategoryTheory.Iso.refl (((HomologicalComplex.single V (ComplexShape.down ℕ) 0).obj X).X 0)
-- Mathlib.Tactic.Translate.Reorder
_private.Mathlib.Tactic.Translate.Reorder.0.Mathlib.Tactic.Translate.Permutation.permute!.cyclicPermuteAux : {α : Type u_1} → Array α → List ℕ → α → ℕ → Array α
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_diff_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ \ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∈ t₂
-- Mathlib.Topology.Order.AtTopBotIxx
/-- The `atBot` filter for an open interval `Ioo a b` comes from the right-neighbourhoods filter at
the left endpoint in the ambient order.  -/
comap_coe_Ioo_nhdsGT : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] (a b : X),
  autoParam (Order.IsPredPrelimit a) comap_coe_Ioo_nhdsGT._auto_1 →
    Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a)) = Filter.atBot
-- Mathlib.RingTheory.Nilpotent.GeometricallyReduced
Algebra.IsGeometricallyReduced.mk : ∀ {R : Type u_3} {A : Type u_4} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  (∀ (p : Ideal R) [inst_3 : p.IsPrime], IsReduced (TensorProduct R (AlgebraicClosure p.ResidueField) A)) →
    Algebra.IsGeometricallyReduced R A
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {fallback : γ},
  Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.map f t) k fallback =
    (Option.map (f k) (Std.ExtDTreeMap.Const.get? t k)).getD fallback
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
CategoryTheory.TwoSquare.lanBaseChange_app : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {D : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] [inst_4 : CategoryTheory.Category.{v₅, u₅} D]
  {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄}
  {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  [inst_5 : ∀ (F : CategoryTheory.Functor C₁ D), L.HasLeftKanExtension F]
  [inst_6 : ∀ (F : CategoryTheory.Functor C₂ D), R.HasLeftKanExtension F] (F : CategoryTheory.Functor C₂ D),
  w.lanBaseChange.app F =
    ((L.lanAdjunction D).homEquiv (((CategoryTheory.Functor.whiskeringLeft C₁ C₂ D).obj T).obj F)
          ((R.lan.comp ((CategoryTheory.Functor.whiskeringLeft C₃ C₄ D).obj B)).obj F)).symm
      (CategoryTheory.StructuredArrow.hom
        ((CategoryTheory.Functor.LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_of_add_le_add_left : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [AddLeftReflectLE α] {a b c : α}, a + b ≤ a + c → b ≤ c
-- Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
PiTensorProduct.ofFinsuppEquiv.eq_1 : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [inst : CommSemiring R] [inst_1 : Fintype ι]
  [inst_2 : DecidableEq ι] [inst_3 : (i : ι) → DecidableEq (κ i)] [inst_4 : (i : ι) → AddCommMonoid (M i)]
  [inst_5 : (i : ι) → Module R (M i)] [inst_6 : (i : ι) → DecidableEq (M i)],
  PiTensorProduct.ofFinsuppEquiv =
    ((PiTensorProduct.congr fun x => finsuppLequivDFinsupp R).trans PiTensorProduct.ofDFinsuppEquiv).trans
      (finsuppLequivDFinsupp R).symm
-- Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
ValuativeRel.not_isNontrivial_of_trivialRel : ∀ {R Γ : Type} [inst : Ring R] [inst_1 : DecidableEq R] [inst_2 : IsDomain R]
  [inst_3 : LinearOrderedCommGroupWithZero Γ] [inst_4 : ValuativeRel R] [Valuation.Compatible 1],
  ¬ValuativeRel.IsNontrivial R
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residueFieldCongr.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} {x y : ↥X} (h : x = y),
  AlgebraicGeometry.Scheme.residueFieldCongr h = AlgebraicGeometry.Scheme.residueFieldCongr h
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.finrank_eq_zero_iff_of_free : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M] [Module.Finite R M], Module.finrank R M = 0 ↔ Subsingleton M
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.brecOn.go : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J RingCat} →
      {motive : RingCat.Colimits.Prequotient F → Sort u} →
        (t : RingCat.Colimits.Prequotient F) →
          ((t : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Prequotient.below t → motive t) →
            motive t ×' RingCat.Colimits.Prequotient.below t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
/-- The formula `x(P₁ + P₂) = x(P₁ - P₂) - ψ(P₁)ψ(P₂) / (x(P₂) - x(P₁))²`,
where `ψ(x,y) = 2y + a₁x + a₃`.  -/
WeierstrassCurve.Affine.addX_eq_addX_negY_sub : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ : F} (y₁ y₂ : F),
  x₁ ≠ x₂ →
    W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) =
      W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂)) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.coe_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X : C},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- For `P : MorphismProperty C`, `P.diagonal` is a morphism property that holds for `f : X ⟶ Y`
whenever `P` holds for `X ⟶ Y xₓ Y`.  -/
CategoryTheory.MorphismProperty.diagonal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_eq_some_iff_exists_beq_and_mem_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k : α} {v : β},
      Std.DHashMap.Internal.Raw₀.Const.get? m k = some v ↔
        ∃ k', (k == k') = true ∧ (k', v) ∈ Std.DHashMap.Raw.Const.toList ↑m
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.rightUnitor_neg_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.AddMon C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).inv
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.neighborSet_singletonSubgraph : ∀ {V : Type u} {G : SimpleGraph V} (v w : V), (G.singletonSubgraph v).neighborSet w = ∅
-- Mathlib.Topology.Algebra.MulAction
IsScalarTower.continuousSMul : ∀ {M : Type u_5} (N : Type u_6) {α : Type u_7} [inst : Monoid N] [inst_1 : SMul M N] [inst_2 : MulAction N α]
  [inst_3 : SMul M α] [IsScalarTower M N α] [inst_5 : TopologicalSpace M] [inst_6 : TopologicalSpace N]
  [inst_7 : TopologicalSpace α] [ContinuousSMul M N] [ContinuousSMul N α], ContinuousSMul M α
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.rightUnitor_inv_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Center C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.f =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.fst).inv
-- Mathlib.Order.Filter.Pointwise
IsAddUnit.filter : ∀ {α : Type u_2} [inst : AddMonoid α] {a : α}, IsAddUnit a → IsAddUnit (pure a)
-- Mathlib.Topology.Algebra.GroupWithZero
Homeomorph.mulRight₀.congr_simp : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : GroupWithZero α] [inst_2 : SeparatelyContinuousMul α] (c c_1 : α)
  (e_c : c = c_1) (hc : c ≠ 0), Homeomorph.mulRight₀ c hc = Homeomorph.mulRight₀ c_1 ⋯
-- Lean.Widget.UserWidget
/-- Retrieve all the `UserWidgetInfo`s that intersect a given line.  -/
Lean.Widget.widgetInfosAt? : Lean.FileMap → Lean.Elab.InfoTree → ℕ → List Lean.Elab.UserWidgetInfo
-- Batteries.Lean.System.IO
/-- Given a list of tasks, create the task returning the list of results,
by waiting for each.
 -/
List.waitAll : {α : Type u_1} → List (Task α) → Task (List α)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.Context.mk.inj : ∀ {α : Lean.Expr} {univ : Lean.Level} {α0 : Lean.Expr} {isGroup : Bool} {inst α_1 : Lean.Expr} {univ_1 : Lean.Level}
  {α0_1 : Lean.Expr} {isGroup_1 : Bool} {inst_1 : Lean.Expr},
  { α := α, univ := univ, α0 := α0, isGroup := isGroup, inst := inst } =
      { α := α_1, univ := univ_1, α0 := α0_1, isGroup := isGroup_1, inst := inst_1 } →
    α = α_1 ∧ univ = univ_1 ∧ α0 = α0_1 ∧ isGroup = isGroup_1 ∧ inst = inst_1
-- Batteries.Data.Char.Basic
Char.all_eq_true_iff_forall_eq_true : ∀ {p : Char → Bool}, Char.all p = true ↔ ∀ (c : Char), p c = true
-- Mathlib.Topology.Algebra.ConstMulAction
/-- The homeomorphism given by affine-addition by an element of an additive group `Γ` acting on
`T` is a homeomorphism from `T` to itself.  -/
Homeomorph.vadd : {α : Type u_2} →
  {G : Type u_4} →
    [inst : TopologicalSpace α] →
      [inst_1 : AddGroup G] → [inst_2 : AddAction G α] → [ContinuousConstVAdd G α] → G → α ≃ₜ α
-- Mathlib.Tactic.IntervalCases
/-- Given `e`, construct `(bound, n, p)` where `p` is a proof of `e ≤ n` or `e < n`
(characterized by `bound`), or `failure` if the type is not upper-bounded.  -/
Mathlib.Tactic.IntervalCases.Methods.initUB : Mathlib.Tactic.IntervalCases.Methods →
  Lean.Expr → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr)
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.instDecidableEqQuaternionGroup.decEq.match_1.eq_2 : ∀ {n : ℕ} (motive : QuaternionGroup n → QuaternionGroup n → Sort u_1) (a a_1 : ZMod (2 * n))
  (h_1 : (a b : ZMod (2 * n)) → motive (QuaternionGroup.a a) (QuaternionGroup.a b))
  (h_2 : (a a_2 : ZMod (2 * n)) → motive (QuaternionGroup.a a) (QuaternionGroup.xa a_2))
  (h_3 : (a a_2 : ZMod (2 * n)) → motive (QuaternionGroup.xa a) (QuaternionGroup.a a_2))
  (h_4 : (a b : ZMod (2 * n)) → motive (QuaternionGroup.xa a) (QuaternionGroup.xa b)),
  (match QuaternionGroup.a a, QuaternionGroup.xa a_1 with
    | QuaternionGroup.a a, QuaternionGroup.a b => h_1 a b
    | QuaternionGroup.a a, QuaternionGroup.xa a_2 => h_2 a a_2
    | QuaternionGroup.xa a, QuaternionGroup.a a_2 => h_3 a a_2
    | QuaternionGroup.xa a, QuaternionGroup.xa b => h_4 a b) =
    h_2 a a_1
-- Mathlib.RingTheory.Nilpotent.Basic
Commute.isNilpotent_sum : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_3} {s : Finset ι} {f : ι → R},
  (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.skip?_eq_some_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} {pos res : s.Pos},
  pos.skip? pat = some res ↔ String.Slice.Pattern.Model.IsLongestMatchAt pat pos res
-- Batteries.Data.DList.Lemmas
Batteries.DList.toList_ofList : ∀ {α : Type u_1} (l : List α), (Batteries.DList.ofList l).toList = l
-- Init.Data.BitVec.Lemmas
BitVec.msb_rotateLeft : ∀ {m w : ℕ} {x : BitVec w}, (x.rotateLeft m).msb = x.getMsbD (m % w)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The short complex `Fun(G, A) --d₁₂--> Fun(G × G, A) --dTwo--> Fun(G × G × G, A)` is
isomorphic to the 2nd short complex associated to the complex of inhomogeneous cochains of `A`.  -/
groupCohomology.isoShortComplexH2 : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        HomologicalComplex.sc (groupCohomology.inhomogeneousCochains A) 2 ≅ groupCohomology.shortComplexH2 A
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.isCycle_iff_sameCycle : ∀ {α : Type u_2} {f : Equiv.Perm α} {x : α}, f x ≠ x → (f.IsCycle ↔ ∀ {y : α}, f.SameCycle x y ↔ f y ≠ y)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_covBy_of_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Injective ⇑f → ∀ {p q : Submodule R M}, p ⋖ q → Submodule.map f p ⋖ Submodule.map f q
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.compLeft_id : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M), B.compLeft LinearMap.id = B
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime]
  [hP₂ : P.LiesOver (Ideal.span {↑p})], P.inertiaDeg ℤ = 1
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.instCommMonoidWithConv : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Semiring C] →
            [inst_3 : Bialgebra R C] →
              [inst_4 : Algebra R A] → [Coalgebra.IsCocomm R C] → CommMonoid (WithConv (C →ₐ[R] A))
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the proof that the forward direction of the 2-isomorphism is equal to
the original 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.IsoLift.eq : Mathlib.Tactic.BicategoryLike.IsoLift → Lean.Expr
-- Mathlib.Data.Int.Bitwise
Int.shiftLeft_neg : ∀ (m n : ℤ), m <<< (-n) = m >>> n
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.mk : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.edges.Nodup → p.IsTrail
-- Lean.Meta.Match.MVarRenaming
Lean.Meta.MVarRenaming.apply : Lean.Meta.MVarRenaming → Lean.Expr → Lean.Expr
-- Mathlib.Geometry.Euclidean.Incenter
/-- The distance between an excenter and a face of the simplex (zero if no such excenter
exists).  -/
Affine.Simplex.exradius : {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 : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → Finset (Fin (n + 1)) → ℝ
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.instAdditiveLocalization'Q' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (W : CategoryTheory.MorphismProperty C) [inst_2 : W.HasLeftCalculusOfFractions] [inst_3 : W.HasLocalization],
  W.Q'.Additive
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instCommRing : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : CommRing R] → (v : Valuation R Γ₀) → CommRing (WithVal v)
-- Batteries.Tactic.Trans
/-- Finds an explicit binary relation in the argument, if possible.  -/
Batteries.Tactic.getRel : Lean.Expr → Lean.MetaM (Option (Batteries.Tactic.TransRelation × Lean.Expr × Lean.Expr))
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.neg_right : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousNeg F],
  f =O[𝕜; l] g → f =O[𝕜; l] (-g)
-- Batteries.Data.List.Lemmas
List.countBefore_idxOfNth_of_lt_count : ∀ {α : Type u_1} {n : ℕ} {x : α} [inst : BEq α] {xs : List α},
  n < List.count x xs → List.countBefore x xs (List.idxOfNth x xs n) = n
-- Init.Data.UInt.Lemmas
UInt32.ofFin_uint8ToFin : ∀ (n : UInt8), UInt32.ofFin (Fin.castLE UInt8.toFin_toUInt32._proof_1 n.toFin) = n.toUInt32
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_bmod_sub_self : ∀ {x : ℤ} {m : ℕ}, ↑m ∣ x.bmod m - x
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.AbsolutelyContinuous.map : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} [inst_4 : MeasureTheory.MeasureSpace β],
  v.AbsolutelyContinuous w → ∀ (f : α → β), (v.map f).AbsolutelyContinuous (w.map f)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonUnitalRing.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : Semigroup M],
  MonoidAlgebra.nonUnitalRing = { toNonUnitalNonAssocRing := MonoidAlgebra.nonUnitalNonAssocRing, mul_assoc := ⋯ }
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.overPullbackMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullbacksAlong f]
  {X Y : CategoryTheory.Over S} (g : X ⟶ Y),
  P (CategoryTheory.Over.Hom.left g) → P (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map g))
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.comp_toLinearMap_eq_iff : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₁ : R₃ →+* R₁} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂}
  [inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (f g : M₃ →ₛₗ[σ₃₁] M₁), ↑e₁₂ ∘ₛₗ f = ↑e₁₂ ∘ₛₗ g ↔ f = g
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The inclusion `Δ[1] ⟶ Λ[2, 2]` which avoids `0`.  -/
SSet.horn₂₂.ι₁₂ : SSet.stdSimplex.obj { len := 1 } ⟶ (SSet.horn 2 2).toSSet
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerRight.default : Mathlib.Tactic.BicategoryLike.WhiskerRight
-- Std.Data.HashSet.Basic
/-- Support for the `for` loop construct in `do` blocks.  -/
Std.HashSet.forIn : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {m : Type v → Type w} → [Monad m] → {β : Type v} → (α → β → m (ForInStep β)) → β → Std.HashSet α → m β
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_apply_apply_pow_self : ∀ {α : Type u_2} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle] (x : α) (k : ℕ),
  (f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x
-- Mathlib.RingTheory.RingHom.QuasiFinite
RingHom.QuasiFinite.respectsIso : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => RingHom.QuasiFinite
-- Mathlib.NumberTheory.Ostrowski
/-- The standard absolute value on `ℚ`. We name it `real` because it corresponds to the
unique real place of `ℚ`.  -/
Rat.AbsoluteValue.real : AbsoluteValue ℚ ℝ
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instReflBEq : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp], ReflBEq (Std.ExtTreeSet α cmp)
-- Lean.Parser.Command
Lean.Parser.Command.declaration.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Set.Countable
Set.enumerateCountable_mem : ∀ {α : Type u} {s : Set α} (h : s.Countable) {default : α},
  default ∈ s → ∀ (n : ℕ), Set.enumerateCountable h default n ∈ s
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β), (↑↑f.toRingHom).toFun = ⇑f
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induceHom_id : ∀ {V : Type u_1} (G : SimpleGraph V) (s : Set V), SimpleGraph.induceHom SimpleGraph.Hom.id ⋯ = SimpleGraph.Hom.id
-- Mathlib.Order.Filter.Interval
Filter.Tendsto.Ioc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {l₁ l₂ : Filter α} [Filter.TendstoIxxClass Set.Ioc l₁ l₂]
  {lb : Filter β} {u₁ u₂ : β → α},
  Filter.Tendsto u₁ lb l₁ → Filter.Tendsto u₂ lb l₁ → Filter.Tendsto (fun x => Set.Ioc (u₁ x) (u₂ x)) lb l₂.smallSets
-- Mathlib.GroupTheory.Goursat
/-- For `I` a subgroup of `G × H`, `I.goursatFst` is the kernel of the projection map `I → H`,
considered as a subgroup of `G`.

This is the first subgroup appearing in Goursat's lemma. See `Subgroup.goursat`.  -/
Subgroup.goursatFst : {G : Type u_1} → {H : Type u_2} → [inst : Group G] → [inst_1 : Group H] → Subgroup (G × H) → Subgroup G