mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.Units
AddUnits.val_vadd : ∀ {G : Type u_1} {M : Type u_3} [inst : AddGroup G] [inst_1 : AddMonoid M] [inst_2 : AddAction G M]
  [inst_3 : VAddCommClass G M M] [inst_4 : VAddAssocClass G M M] (g : G) (m : AddUnits M), ↑(g +ᵥ m) = g +ᵥ ↑m
-- Mathlib.Data.Matrix.Mul
Matrix.sub_vecMulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocRing α] (w₁ w₂ : m → α) (v : n → α),
  Matrix.vecMulVec (w₁ - w₂) v = Matrix.vecMulVec w₁ v - Matrix.vecMulVec w₂ v
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- The type of 2-squares on functors `T`, `L`, `R`, and `B` is trivially equivalent to
the type of natural transformations `T ⋙ R ⟶ L ⋙ B`.  -/
CategoryTheory.TwoSquare.equivNatTrans : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : 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₄] →
                (T : CategoryTheory.Functor C₁ C₂) →
                  (L : CategoryTheory.Functor C₁ C₃) →
                    (R : CategoryTheory.Functor C₂ C₄) →
                      (B : CategoryTheory.Functor C₃ C₄) → CategoryTheory.TwoSquare T L R B ≃ (T.comp R ⟶ L.comp B)
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `Equiv.cast (congrArg _ h)` as an `AddEquiv`.

Note that unlike `Equiv.cast`, this takes an equality of indices rather than an equality of types,
to avoid having to deal with an equality of the algebraic structure itself.  -/
AddEquiv.cast : {ι : Type u_9} → {M : ι → Type u_10} → [inst : (i : ι) → Add (M i)] → {i j : ι} → i = j → M i ≃+ M j
-- Batteries.Data.List.Lemmas
List.prod_pair : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] [Std.LawfulRightIdentity (fun x1 x2 => x1 * x2) 1] {a b : α},
  [a, b].prod = a * b
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.yonedaCollectionFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v))
  (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)),
  (CategoryTheory.OverPresheafAux.yonedaCollectionFunctor A).obj F =
    CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F
-- Mathlib.Data.Finset.Card
/-- To prove a proposition for an arbitrary `Finset α`,
it suffices to prove that for any `S : Finset α`, the following is true:
the property is true for S with any element `s` removed, then the property holds for `S`.

This is a weaker version of `Finset.strongInduction`.
But it can be more precise when the induction argument
only requires removing single elements at a time.
 -/
Finset.eraseInduction : ∀ {α : Type u_1} [inst : DecidableEq α] {p : Finset α → Prop},
  (∀ (S : Finset α), (∀ s ∈ S, p (S.erase s)) → p S) → ∀ (S : Finset α), p S
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_comp_cycle : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  {P : Type u_4} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : AddCommGroup P] [inst_6 : Module R P]
  [Module.Free R N] [Module.Finite R N] [Module.Free R P] [Module.Finite R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P)
  (h : P →ₗ[R] M), (LinearMap.trace R P) (g ∘ₗ f ∘ₗ h) = (LinearMap.trace R N) (f ∘ₗ h ∘ₗ g)
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.toDigitsCore.match_1.splitter : (motive : ℕ → ℕ → List Char → Sort u_1) →
  (x x_1 : ℕ) →
    (x_2 : List Char) →
      ((x : ℕ) → (ds : List Char) → motive 0 x ds) →
        ((fuel n : ℕ) → (ds : List Char) → motive fuel.succ n ds) → motive x x_1 x_2
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The set of conjugates of the union of two sets is the union of the conjugates  -/
Group.conjugatesOfSet_union : ∀ {G : Type u_5} [inst : Group G] (s t : Set G),
  Group.conjugatesOfSet (s ∪ t) = Group.conjugatesOfSet s ∪ Group.conjugatesOfSet t
-- Mathlib.Analysis.PSeries
/-- Harmonic series is not unconditionally summable.  -/
Real.not_summable_one_div_natCast : ¬Summable fun n => 1 / ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The first projection of a pullback cone.  -/
CategoryTheory.Limits.PullbackCone.fst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → {f : X ⟶ Z} → {g : Y ⟶ Z} → (t : CategoryTheory.Limits.PullbackCone f g) → t.pt ⟶ X
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_toAlgHom : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ⇑↑e = ⇑e
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_X_left_apply : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R), (MvPolynomial.aeval MvPolynomial.X) p = p
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ofObjects_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C), CategoryTheory.Sieve.ofObjects id X = ⊤
-- Lean.Server.InfoUtils
Lean.Elab.GoalsAtResult.priority : Lean.Elab.GoalsAtResult → ℕ
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The space of tempered distribution is the space of continuous linear maps from the Schwartz to
a normed space, equipped with the topology of pointwise convergence.  -/
TemperedDistribution : (E : Type u_3) →
  (F : Type u_4) →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] → [TopologicalSpace F] → [inst : AddCommGroup F] → [Module ℂ F] → Type (max u_3 u_4)
-- Mathlib.Order.Hom.WithTopBot
OrderEmbedding.withTopMap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β),
  f.withTopMap =
    { toEmbedding := { toFun := WithTop.map ⇑f, inj' := ⋯, map_rel_iff' := ⋯ }.toEmbedding, map_rel_iff' := ⋯ }
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_tmul : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] (f : M →ₗ[R] N) (a : A) (x : M), (LinearMap.baseChange A f) (a ⊗ₜ[R] x) = a ⊗ₜ[R] f x
-- Mathlib.Tactic.Linter.Whitespace
/-- Add a new `FormatError` `f` to the array `fs`, trying, as much as possible, to merge the new
`FormatError` with the last entry of `fs`.
 -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.pushFormatError : Array Mathlib.Linter.FormatError✝ → Mathlib.Linter.FormatError✝ → Array Mathlib.Linter.FormatError✝
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.K : Std.Time.GenericFormat.DateBuilder✝ → Option (Std.Time.Internal.Bounded.LE 0 11)
-- Mathlib.Algebra.Order.SuccPred
antitoneOn_of_add_one_le : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : One α]
  [inst_4 : SuccAddOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) ≤ f a) → AntitoneOn f s
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The homology of a short complex `S` identifies to the cokernel of the induced morphism
`S.X₁ ⟶ kernel S.g`.  -/
CategoryTheory.ShortComplex.homologyIsoCokernelLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasHomology] →
          [inst_3 : CategoryTheory.Limits.HasKernel S.g] →
            [inst_4 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)] →
              S.homology ≅ CategoryTheory.Limits.cokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_le_mk_of_abs : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  |a| ≤ |b| → ArchimedeanClass.mk b ≤ ArchimedeanClass.mk a
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileChangeType.noConfusionType : Sort v✝ → Lean.Lsp.FileChangeType → Lean.Lsp.FileChangeType → Sort v✝
-- Mathlib.Analysis.InnerProductSpace.Basic
norm_eq_sqrt_re_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), ‖x‖ = √(RCLike.re (inner 𝕜 x x))
-- Batteries.Data.List.Perm
List.decidableSubperm : {α : Type u_1} → [inst : BEq α] → [LawfulBEq α] → DecidableRel fun x1 x2 => x1.Subperm x2
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.stalkClosedPointIso_inv : ∀ (R : CommRingCat) [inst : IsLocalRing ↑R],
  (AlgebraicGeometry.stalkClosedPointIso R).inv =
    AlgebraicGeometry.StructureSheaf.toStalk (↑R) (IsLocalRing.closedPoint ↑R)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Mul α] [inst_4 : Mul β] [inst_5 : Mul γ] {g : α ≃*o β} {f₁ f₂ : β ≃*o γ},
  Function.Surjective ⇑g → (g.trans f₁ = g.trans f₂ ↔ f₁ = f₂)
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Semiring.mulFn? : Lean.Meta.Sym.Arith.Semiring → Option Lean.Expr
-- Mathlib.Condensed.Discrete.Module
LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf : ∀ (R : Type u) [inst : Ring R],
  (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)).Faithful
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHomClass.toBoundedOrderHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Lattice α] [inst_2 : Lattice β]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [BoundedLatticeHomClass F α β], BoundedOrderHomClass F α β
-- Mathlib.Data.FinEnum
FinEnum.Finset.enum.eq_1 : ∀ {α : Type u} [inst : DecidableEq α], FinEnum.Finset.enum [] = [∅]
-- Init.Data.List.Basic
/-- Auxiliary for `findIdx`: `findIdx.go p l n = findIdx p l + n`  -/
List.findIdx.go : {α : Type u} → (α → Bool) → List α → ℕ → ℕ
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffAt.finsum_section_of_locallyFinite : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {x₀ : M} {ι : Type u_7} {t : ι → (x : M) → V x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) →
    (∀ (i : ι), ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t i x⟩) x₀) →
      ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv1.lt_of_get?_eq_some : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] [EquivBEq α] {n m : ℕ} (map : Std.HashMap α ℕ) (x : α),
  Std.Sat.AIG.RelabelNat.State.Inv1 n map → map[x]? = some m → m < n
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.prop_single : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.single f f
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageActionItem.mk.injEq : ∀ (title title_1 : String), ({ title := title } = { title := title_1 }) = (title = title_1)
-- Init.Data.Int.Order
Int.toNat_lt : ∀ {n : ℕ} {z : ℤ}, 0 ≤ z → (z.toNat < n ↔ z < ↑n)
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f` is a submersion at `x` and `g = f` on some neighbourhood of `x`,
then `g` is a submersion at `x`.  -/
Manifold.IsSubmersionAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N}
  {x : M}, Manifold.IsSubmersionAt I J n f x → f =ᶠ[nhds x] g → Manifold.IsSubmersionAt I J n g x
-- Mathlib.GroupTheory.Perm.List
List.support_formPerm_le : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) [inst_1 : Fintype α], l.formPerm.support ⊆ l.toFinset
-- Mathlib.Data.FP.Basic
FP.FloatCfg.emax : [self : FP.FloatCfg] → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.reflexivePair.match_1.eq_2 : ∀ (motive : CategoryTheory.Limits.WalkingReflexivePair → Sort u_1)
  (h_1 : Unit → motive CategoryTheory.Limits.WalkingReflexivePair.zero)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingReflexivePair.one),
  (match CategoryTheory.Limits.WalkingReflexivePair.one with
    | CategoryTheory.Limits.WalkingReflexivePair.zero => h_1 ()
    | CategoryTheory.Limits.WalkingReflexivePair.one => h_2 ()) =
    h_2 ()
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.ExceptType.tooSmall : Mathlib.Tactic.Ring.ExceptType
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_hom_inv_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) (k : c ⟶ d),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η.hom k))
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η.inv k)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g k))
-- Mathlib.Algebra.Order.Group.PosPart
/-- **Alias** of the reverse direction of `oneLePart_eq_one`. -/
oneLePart_of_le_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] {a : α}, a ≤ 1 → a⁺ᵐ = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.neg_def : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} (P : W.Point), -P = P.neg
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion.0.Tactic.ComputeAsymptotics.Seq.FriendlyOperation.coind_comp_friend_right.match_1_1.splitter : {α : Type u_1} →
  (motive : Option (α × Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation) → Sort u_2) →
    (x : Option (α × Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation)) →
      (Unit → motive none) →
        ((hd : α) → (opf' : Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation) → motive (some (hd, opf'))) →
          motive x
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- A non-unital subalgebra closed under `star` is a non-unital star subalgebra.  -/
NonUnitalSubalgebra.toNonUnitalStarSubalgebra : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : Star A] → (s : NonUnitalSubalgebra R A) → (∀ x ∈ s, star x ∈ s) → NonUnitalStarSubalgebra R A
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiff.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieGroup I n G] {f : M → G}, ContMDiff I' I n f → ContMDiff I' I n fun x => (f x)⁻¹
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.mk.inj : ∀ {α : Type} {state state_1 : Std.Mutex (Std.Bounded.State✝ α)},
  { state := state } = { state := state_1 } → state = state_1
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Print a premise as a string.  -/
Mathlib.Tactic.ClickSuggestions.Premise.toString : Mathlib.Tactic.ClickSuggestions.Premise → String
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instRightCancelMonoid : {α : Type u_1} → [RightCancelMonoid α] → RightCancelMonoid αᵒᵈ
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.pullbackAwayιIso.congr_simp : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m')
  (hm' : 0 < m') {x : A} (hx : x = f * g),
  AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx =
    AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.breakToTerm : Lean.Elab.Term.Do.ToTerm.M Lean.Syntax
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instEpiModuleCatToModuleCatHom : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B)
  [CategoryTheory.Epi f], CategoryTheory.Epi (Rep.Hom.toModuleCatHom f)
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule_inf_invtSubmodule_le_invtSubmodule_add : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f g : Module.End R M), f.invtSubmodule ⊓ g.invtSubmodule ≤ (f + g).invtSubmodule
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.instIsMonHomLift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N O : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] [inst_4 : CategoryTheory.MonObj O]
  [inst_5 : CategoryTheory.BraidedCategory C] {f : M ⟶ N} {g : M ⟶ O} [CategoryTheory.IsMonHom f]
  [CategoryTheory.IsMonHom g], CategoryTheory.IsMonHom (CategoryTheory.CartesianMonoidalCategory.lift f g)
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- If a cospan is the pushout cospan under the initial object, then it is a binary coproduct.  -/
isBinaryCoproductOfIsInitialIsPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) →
      (c : CategoryTheory.Limits.Cocone F) →
        {X : C} →
          (hX : CategoryTheory.Limits.IsInitial X) →
            (f : X ⟶ F.obj { as := CategoryTheory.Limits.WalkingPair.left }) →
              (g : X ⟶ F.obj { as := CategoryTheory.Limits.WalkingPair.right }) →
                CategoryTheory.Limits.IsColimit
                    (CategoryTheory.Limits.PushoutCocone.mk (c.ι.app { as := CategoryTheory.Limits.WalkingPair.left })
                      (c.ι.app { as := CategoryTheory.Limits.WalkingPair.right }) ⋯) →
                  CategoryTheory.Limits.IsColimit c
-- Mathlib.Algebra.Group.TypeTags.Basic
ofAdd_toAdd : ∀ {α : Type u} (x : Multiplicative α), Multiplicative.ofAdd (Multiplicative.toAdd x) = x
-- Batteries.Data.Fin.Lemmas
Fin.eq_true_of_findRev?_eq_some : ∀ {n : ℕ} {i : Fin n} {p : Fin n → Bool}, Fin.findRev? p = some i → p i = true
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.snd_comp_inr : ∀ {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},
  (Representation.IntertwiningMap.snd A ρ σ).comp (Representation.IntertwiningMap.inr A ρ σ) =
    Representation.IntertwiningMap.id σ
-- Mathlib.Data.Multiset.AddSub
Multiset.sub_le_sub_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s ≤ t → s - u ≤ t - u
-- Mathlib.Logic.Function.FromTypes
Function.fromTypes_nil_equiv_apply : ∀ (τ : Type u) (a : Function.FromTypes ![] τ), (Function.fromTypes_nil_equiv τ) a = a
-- Mathlib.Topology.Path
Path.map_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} (γ : Path x y)
  {f : X → Y} (h : Continuous f), ⇑(γ.map h) = f ∘ ⇑γ
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.prime_of_factor : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
  ∀ x ∈ UniqueFactorizationMonoid.factors a, Prime x
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedSup_union_right : ∀ {α : Type u_1} [inst : SemilatticeSup α] {s t : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : OrderTop α]
  [inst_3 : DecidableEq α], a ∉ lowerClosure ↑s → a ∈ lowerClosure ↑t → (s ∪ t).truncatedSup a = t.truncatedSup a
-- Mathlib.Data.Set.Basic
Set.Nonempty.inl : ∀ {α : Type u} {s t : Set α}, s.Nonempty → (s ∪ t).Nonempty
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k a : α} [inst_3 : Inhabited (β a)] {v : β k},
      (m.insertIfNew k v).get! a = if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.get! a
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Set.toFinset_smul_set : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] (a : α) (s : Set β) [inst_2 : Fintype ↑s]
  [inst_3 : Fintype ↑(a • s)], (a • s).toFinset = a • s.toFinset
-- Mathlib.Algebra.Order.Group.OrderIso
/-- `x ↦ -x` as an order-reversing equivalence.  -/
OrderIso.neg : (α : Type u) → [inst : AddGroup α] → [inst_1 : LE α] → [AddLeftMono α] → [AddRightMono α] → α ≃o αᵒᵈ
-- Mathlib.Topology.Connected.Basic
/-- The universal set `Set.univ` in a preconnected space is a preconnected set.  -/
PreconnectedSpace.isPreconnected_univ : ∀ {α : Type u} {inst : TopologicalSpace α} [self : PreconnectedSpace α], IsPreconnected Set.univ
-- Mathlib.CategoryTheory.Functor.Flat
/-- A functor `F : C ⥤ D` is representably coflat if the comma category `(F/X)` is filtered for
each `X : D`.  -/
CategoryTheory.RepresentablyCoflat : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- `A.submatrix e₁ e₂` is invertible if `A` is  -/
Matrix.submatrixEquivInvertible : {m : Type u} →
  {n : Type u'} →
    {α : Type v} →
      [inst : Fintype n] →
        [inst_1 : DecidableEq n] →
          [inst_2 : CommRing α] →
            [inst_3 : Fintype m] →
              [inst_4 : DecidableEq m] →
                (A : Matrix m m α) → (e₁ e₂ : n ≃ m) → [Invertible A] → Invertible (A.submatrix ⇑e₁ ⇑e₂)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [P.IsClosedUnderColimitsOfShape Jᵒᵖ], P.op.IsClosedUnderLimitsOfShape J
-- Init.Data.List.Lemmas
List.append_right_inj : ∀ {α : Type u_1} {t₁ t₂ : List α} (s : List α), s ++ t₁ = s ++ t₂ ↔ t₁ = t₂
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_succ_Ico : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.succ (Finset.Ico i j) = Finset.Ico i.succ j.succ
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.instCountableDiscreteQuotient : ∀ (S : LightProfinite), Countable (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)