mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.ofArray_eq_of_getD : ∀ {R : Type u_7} [inst : Zero R] {m n : ℕ} (A : Array R) (hA : A.size = m * n),
  Matrix.ofArray A hA = Matrix.of fun i j => A.getD (n * ↑i + ↑j) 0
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory : {V : Type u'} →
  {inst : CategoryTheory.Category.{v', u'} V} →
    {inst_1 : CategoryTheory.MonoidalCategory V} →
      {C : Type u} →
        {inst_2 : CategoryTheory.Category.{v, u} C} →
          [self : CategoryTheory.EnrichedOrdinaryCategory V C] → CategoryTheory.EnrichedCategory V C
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- This definition allows the replacement of the `ι` field of
a `AttachCells g f` structure by an equivalent type.  -/
HomotopicalAlgebra.AttachCells.reindex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} →
            {f : X₁ ⟶ X₂} →
              (c : HomotopicalAlgebra.AttachCells g f) → {ι' : Type w'} → ι' ≃ c.ι → HomotopicalAlgebra.AttachCells g f
-- Mathlib.FieldTheory.IsSepClosed
/-- If `E` is separably closed, then the separable closure of `F` in `E` is an absolute
separable closure of `F`.  -/
separableClosure.isSepClosure : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsSepClosed E],
  IsSepClosure F ↥(separableClosure F E)
-- Mathlib.Algebra.Group.End
AddAutAdditive_apply_apply : ∀ (G : Type u_3) [inst : Group G] (a : Additive G ≃+ Additive G) (a_1 : G),
  ((AddAutAdditive G) a) a_1 = Additive.toMul (a (Additive.ofMul a_1))
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_real_interval : ∀ {a b : ℝ}, MeasureTheory.volume.real (Set.uIcc a b) = |b - a|
-- Mathlib.Topology.Algebra.Monoid
continuousAdd_of_comm_of_nhds_zero : ∀ (M : Type u) [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
    (∀ (x₀ : M), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) → ContinuousAdd M
-- Mathlib.Algebra.GroupWithZero.Defs
CancelMonoidWithZero.mk.injEq : ∀ {M₀ : Type u_2} (toMonoidWithZero : MonoidWithZero M₀) (toIsCancelMulZero : IsCancelMulZero M₀)
  (toMonoidWithZero_1 : MonoidWithZero M₀) (toIsCancelMulZero_1 : IsCancelMulZero M₀),
  ({ toMonoidWithZero := toMonoidWithZero, toIsCancelMulZero := toIsCancelMulZero } =
      { toMonoidWithZero := toMonoidWithZero_1, toIsCancelMulZero := toIsCancelMulZero_1 }) =
    (toMonoidWithZero = toMonoidWithZero_1)
-- Init.Prelude
/-- Extract the right conjunct from a conjunction. `h : a ∧ b` then
`h.right`, also notated as `h.2`, is a proof of `b`.  -/
And.right : ∀ {a b : Prop}, a ∧ b → b
-- Mathlib.Algebra.Category.Ring.Limits
/-- If `(F ⋙ forget CommRingCat).sections` is `u`-small, `F` has a limit.  -/
CommRingCat.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommRingCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections], CategoryTheory.Limits.HasLimit F
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- This is another convenient method to verify that a pullback cone is a limit cone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same `s` for all parts.  -/
CategoryTheory.Limits.PullbackCone.isLimitAux' : {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) →
            ((s : CategoryTheory.Limits.PullbackCone f g) →
                { l //
                  CategoryTheory.CategoryStruct.comp l t.fst = s.fst ∧
                    CategoryTheory.CategoryStruct.comp l t.snd = s.snd ∧
                      ∀ {m : s.pt ⟶ t.pt},
                        CategoryTheory.CategoryStruct.comp m t.fst = s.fst →
                          CategoryTheory.CategoryStruct.comp m t.snd = s.snd → m = l }) →
              CategoryTheory.Limits.IsLimit t
-- Lean.Meta.Eqns
Lean.Meta.backward.eqns.deepRecursiveSplit : Lean.Option Bool
-- Mathlib.CategoryTheory.Whiskering
/-- If `α : G ≅ H` is a natural isomorphism then
`isoWhiskerLeft F α : (F ⋙ G) ≅ (F ⋙ H)` has components `α.app (F.obj X)`.
 -/
CategoryTheory.Functor.isoWhiskerLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) → {G H : CategoryTheory.Functor D E} → (G ≅ H) → (F.comp G ≅ F.comp H)
-- Mathlib.Computability.Partrec
Partrec₂.unpaired : ∀ {α : Type u_1} [inst : Primcodable α] {f : ℕ → ℕ →. α}, Partrec (Nat.unpaired f) ↔ Partrec₂ f
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.ofBraided_map_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Center.ofBraided C).map f).f = f
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpacePUnit : UniformSpace PUnit.{u_2 + 1}
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.prod_symm_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type w} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {E' : Type v'}
  [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {H' : Type w'} [inst_6 : TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H') (x : E × E'), ↑(I.prod I').symm x = (↑I.symm x.1, ↑I'.symm x.2)
-- Mathlib.NumberTheory.NumberField.Discriminant.Defs
NumberField.discr_eq_discr_of_ringEquiv : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {L : Type u_2} [inst_2 : Field L] [inst_3 : NumberField L]
  (f : K ≃+* L), NumberField.discr K = NumberField.discr L
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.eq_on_support_mem_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {l : List (Equiv.Perm α)},
  f ∈ l → List.Pairwise Equiv.Perm.Disjoint l → ∀ x ∈ f.support, f x = l.prod x
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.length_nil : ∀ {V : Type u} [inst : Quiver V] {a : V}, Quiver.Path.nil.length = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_eq_of_tan_eq : ∀ {x y : ℝ}, Real.tan x = y → x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2) → Real.arctan y = x
-- Lean.Elab.App
Lean.Elab.Term.throwInvalidNamedArg : {α : Type} → Lean.Elab.Term.NamedArg → Option Lean.Name → Array Lean.Name → Lean.Elab.TermElabM α
-- Mathlib.Topology.Instances.AddCircle.Defs
toIcoMod_eventuallyEq_toIocMod : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜},
  ¬x ≡ a [PMOD p] → toIcoMod hp a =ᶠ[nhds x] toIocMod hp a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_erase_eq_iff_not_compare_eq_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).maxKey? = t.maxKey? ↔ ∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_span_of_mem : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
  {x : M}, x ∈ s → x ∈ Submodule.span R s
-- Mathlib.Topology.Algebra.GroupWithZero
/-- Right multiplication by a nonzero element in a `GroupWithZero` with continuous multiplication
is a homeomorphism of the underlying type.  -/
Homeomorph.mulRight₀ : {α : Type u_1} →
  [inst : TopologicalSpace α] → [inst_1 : GroupWithZero α] → [SeparatelyContinuousMul α] → (c : α) → c ≠ 0 → α ≃ₜ α
-- Mathlib.Algebra.Category.AlgCat.FilteredColimits
instHasColimitsOfShapeAlgCatOfIsFilteredOfRingCat : ∀ {R : Type u} [inst : CommRing R] {J : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} J]
  [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget RingCat)] [CategoryTheory.IsFiltered J]
  [CategoryTheory.Limits.HasColimitsOfShape J RingCat], CategoryTheory.Limits.HasColimitsOfShape J (AlgCat R)
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.uint64.sizeOf_spec : sizeOf Lean.IR.IRType.uint64 = 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.adjoin_range_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, Algebra.adjoin R (Set.range ⇑(CliffordAlgebra.ι Q)) = ⊤
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.sub_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ - 0 = μ
-- Mathlib.RingTheory.Ideal.Quotient.Basic
/-- The quotient of a ring by an ideal is a field iff the ideal is maximal.  -/
Ideal.Quotient.maximal_ideal_iff_isField_quotient : ∀ {R : Type u_5} [inst : CommRing R] (I : Ideal R), I.IsMaximal ↔ IsField (R ⧸ I)
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsSemisimple.add_of_commute : ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f g : Module.End K M}
  [FiniteDimensional K M] [PerfectField K], Commute f g → f.IsSemisimple → g.IsSemisimple → (f + g).IsSemisimple
-- Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
/-- If `E` is first countable, then every locally bounded linear map `E →ₛₗ[σ] F` is continuous.  -/
LinearMap.continuous_of_locally_bounded : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [inst_3 : AddCommGroup F] [inst_4 : TopologicalSpace F] [inst_5 : NontriviallyNormedField 𝕜]
  [inst_6 : Module 𝕜 E] [ContinuousSMul 𝕜 E] [inst_8 : NormedField 𝕜'] [inst_9 : Module 𝕜' F] {σ : 𝕜 →+* 𝕜'}
  [RingHomIsometric σ] [FirstCountableTopology E] [IsTopologicalAddGroup F] (f : E →ₛₗ[σ] F),
  (∀ (s : Set E), Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜' (⇑f '' s)) → Continuous ⇑f
-- Mathlib.FieldTheory.NormalizedTrace
Algebra.normalizedTrace_self : ∀ (F : Type u_1) [inst : Field F] [inst_1 : CharZero F], Algebra.normalizedTrace F F = LinearMap.id
-- Init.Data.SInt.Lemmas
Int32.ofInt_neg : ∀ (a : ℤ), Int32.ofInt (-a) = -Int32.ofInt a
-- Mathlib.Data.Sym.Sym2
Set.sym2_insert : ∀ {α : Type u_1} (a : α) (s : Set α), (insert a s).sym2 = (fun b => s(a, b)) '' insert a s ∪ s.sym2
-- Mathlib.Algebra.Group.Basic
/-- To show a property of all powers of `g` it suffices to show it is closed under multiplication
by `g` and `g⁻¹` on the left. For subgroups generated by more than one element, see
`Subgroup.closure_induction_left`.  -/
zpow_induction_left : ∀ {G : Type u_3} [inst : Group G] {g : G} {P : G → Prop},
  P 1 → (∀ (a : G), P a → P (g * a)) → (∀ (a : G), P a → P (g⁻¹ * a)) → ∀ (n : ℤ), P (g ^ n)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.sub_notMem_range_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [CharZero R] {i j : ι}, i ∈ b.support → j ∈ b.support → P.coroot i - P.coroot j ∉ Set.range ⇑P.coroot
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- An isomorphism to describe the action of `RightExtension.postcompose₂` on terms of the form
`RightExtension.mk _ α`.  -/
CategoryTheory.Functor.RightExtension.postcompose₂ObjMkIso : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                {L : CategoryTheory.Functor C D} →
                  {F : CategoryTheory.Functor C H} →
                    (G : CategoryTheory.Functor H D') →
                      {F' : CategoryTheory.Functor D H} →
                        (α : L.comp F' ⟶ F) →
                          (CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj
                              (CategoryTheory.Functor.RightExtension.mk F' α) ≅
                            CategoryTheory.Functor.RightExtension.mk (F'.comp G)
                              (CategoryTheory.CategoryStruct.comp (L.associator F' G).inv
                                (CategoryTheory.Functor.whiskerRight α G))
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.coe_mulBialgHom : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Bialgebra R A],
  ⇑(Bialgebra.mulBialgHom R A) = ⇑(LinearMap.mul' R A)
-- Std.Sat.AIG.CNF
/-- `State.Inv` holds for the CNF that we produce for a `Decl.gate`
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.Inv_gateToCNF : ∀ {upper : ℕ} {lhs rhs : Std.Sat.AIG.Fanin} {aig : Std.Sat.AIG ℕ} {h : upper < aig.decls.size},
  aig.decls[upper] = Std.Sat.AIG.Decl.gate lhs rhs →
    Std.Sat.AIG.toCNF.State.Inv✝ aig (Std.Sat.AIG.Decl.gateToCNF✝ upper lhs.gate rhs.gate lhs.invert rhs.invert)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- This is a convenient constructor for `Away 𝒜 f` when `f` is homogeneous.
`Away.mk 𝒜 hf n x hx` is the fraction `x / f ^ n`.  -/
HomogeneousLocalization.Away.mk : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                (𝒜 : ι → σ) →
                  [GradedRing 𝒜] →
                    {f : A} → {d : ι} → f ∈ 𝒜 d → (n : ℕ) → (x : A) → x ∈ 𝒜 (n • d) → HomogeneousLocalization.Away 𝒜 f
-- Mathlib.CategoryTheory.Action.Concrete
/-- Specialize `instMulAction` to assist typeclass inference.  -/
Action.instMulActionObjFiniteVFintypeCat : {G : Type u_3} → [inst : Monoid G] → (X : Action FintypeCat G) → MulAction G X.V.obj
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.mulIndicator_apply_eq_if : ∀ {X : Type u_1} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : One R] {U : Set X} (f : LocallyConstant X R)
  (a : X) (hU : IsClopen U), (f.mulIndicator hU) a = if a ∈ U then f a else 1
-- Lean.Attributes
Lean.AttributeKind.noConfusionType : Sort v✝ → Lean.AttributeKind → Lean.AttributeKind → Sort v✝
-- Aesop.Tree.Data
Aesop.Rapp.depth : Aesop.Rapp → BaseIO ℕ
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- The class of transfinite compositions (for arbitrary well-ordered types `J : Type w`)
of a class of morphisms `W`.  -/
CategoryTheory.MorphismProperty.transfiniteCompositions : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- One can reformulate smoothness within a set at a point as continuity within this set at this
point, and smoothness in the corresponding extended chart. This form states smoothness of `f`
written in such a way that the set is restricted to lie within the domain/codomain of the
corresponding charts.
Even though this expression is more complicated than the one in `mdifferentiableWithinAt_iff`, it is
a smaller set, but their germs at `extChartAt I x x` are equal. It is sometimes useful to rewrite
using this in the goal.
 -/
mdifferentiableWithinAt_iff_target_inter' : ∀ {𝕜 : 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'] {f : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
        ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
        (↑(extChartAt I x) x)
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.hilbertPoly_mul_one_sub_pow_add : ∀ {F : Type u_1} [inst : Field F] [CharZero F] (p : Polynomial F) (d e : ℕ),
  (p * (1 - Polynomial.X) ^ e).hilbertPoly (d + e) = p.hilbertPoly d
-- Std.Data.HashMap.Basic
/-- Creates a hash map from a list of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofList`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.  -/
Std.HashMap.unitOfList : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → List α → Std.HashMap α Unit
-- Mathlib.GroupTheory.MonoidLocalization.Lemmas
/-- See also the analogous `IsLocalization.map_integerMultiple`.  -/
Submonoid.IsLocalizationMap.surj_pi_of_finite : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_3} {ι : Type u_4} [Finite ι] [inst : CommMonoid M] [inst_1 : CommMonoid N]
  [inst_2 : FunLike F M N] [MulHomClass F M N] {f : F} {S : Submonoid M},
  S.IsLocalizationMap ⇑f → ∀ (n : ι → N), ∃ s x, ∀ (i : ι), n i * f ↑s = f (x i)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.homCategory.ext_iff : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {m n : η ⟶ θ}, m = n ↔ ∀ (b : B), m.as.app b = n.as.app b
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The forgetful functor from module objects to the ambient category.  -/
CategoryTheory.Mod.forget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            (A : C) → [inst_4 : CategoryTheory.MonObj A] → CategoryTheory.Functor (CategoryTheory.Mod D A) D
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_Φ_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [Nontrivial R] (n : ℤ), (W.Φ n).coeff (n.natAbs ^ 2) ≠ 0
-- Mathlib.Probability.HasLawExists
ProbabilityTheory.exists_iid : ∀ (ι : Type v) {𝓧 : Type u} {m𝓧 : MeasurableSpace 𝓧} (μ : MeasureTheory.Measure 𝓧)
  [MeasureTheory.IsProbabilityMeasure μ],
  ∃ Ω x P X,
    (∀ (i : ι), Measurable (X i)) ∧
      (∀ (i : ι), ProbabilityTheory.HasLaw (X i) μ P) ∧
        ProbabilityTheory.iIndepFun X P ∧ MeasureTheory.IsProbabilityMeasure P
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.smul_mem_pointwise_smul : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] (m : M) (a : α)
  (S : Submodule R M), m ∈ S → a • m ∈ a • S
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.integral_sub_right_eq_self : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure G} [inst_3 : AddGroup G] [MeasurableAdd G] [μ.IsAddRightInvariant] (f : G → E) (g : G),
  ∫ (x : G), f (x - g) ∂μ = ∫ (x : G), f x ∂μ
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.sum_zero_index : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {S : Type u_3} [inst_1 : AddCommMonoid S] {f : G → k → S},
  SkewMonoidAlgebra.sum 0 f = 0
-- Mathlib.Data.Finset.NatDivisors
Nat.Prime.divisors_sq : ∀ {p : ℕ}, Nat.Prime p → (p ^ 2).divisors = {p ^ 2, p, 1}
-- Mathlib.Analysis.Calculus.FDeriv.Pow
/-- Eta-expanded form of `HasFDerivWithinAt.pow'` -/
HasFDerivWithinAt.fun_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {f' : E →L[𝕜] 𝔸}
  {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x →
    ∀ (n : ℕ),
      HasFDerivWithinAt (fun i => f i ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') s
        x
-- Lean.Widget.InteractiveCode
/-- In certain situations such as when goal states change between positions in a tactic-mode proof,
we can show subexpression-level diffs between two expressions. This field asks the renderer to
display the subexpression as in a diff view (e.g. red/green like `git diff`).  -/
Lean.Widget.SubexprInfo.diffStatus? : Lean.Widget.SubexprInfo → Option Lean.Widget.DiffTag
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m₁ \ m₂).contains k = (m₁.contains k && !m₂.contains k)
-- Mathlib.Order.Minimal
IsLeast.minimal_iff : ∀ {α : Type u_2} {a x : α} {s : Set α} [inst : PartialOrder α], IsLeast s a → (Minimal (fun x => x ∈ s) x ↔ x = a)
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_zsmul : ∀ {R : Type u} [inst : AddGroup R] (x : R) (n : ℤ), Tropical.trop (n • x) = Tropical.trop x ^ n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_smul_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P Q : Fin 3 → R) {u v : R},
  IsUnit u → IsUnit v → W'.add (u • P) (v • Q) ≈ W'.add P Q
-- Mathlib.Computability.Primrec.Basic
Primrec₂.comp₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {σ : Type u_5} [inst : Primcodable α]
  [inst_1 : Primcodable β] [inst_2 : Primcodable γ] [inst_3 : Primcodable δ] [inst_4 : Primcodable σ] {f : γ → δ → σ}
  {g : α → β → γ} {h : α → β → δ}, Primrec₂ f → Primrec₂ g → Primrec₂ h → Primrec₂ fun a b => f (g a b) (h a b)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.negMulLog_mul : ∀ (x y : ℝ), (x * y).negMulLog = y * x.negMulLog + x * y.negMulLog
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure_C_mul : ∀ {a : ℂ},
  a ≠ 0 → ∀ {p : Polynomial ℂ}, p ≠ 0 → (Polynomial.C a * p).logMahlerMeasure = Real.log ‖a‖ + p.logMahlerMeasure
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.diagonal_isStableUnderComposition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderComposition] [P.RespectsIso] [P.IsStableUnderBaseChange],
  P.diagonal.IsStableUnderComposition
-- Mathlib.CategoryTheory.Category.ULift
/-- The equivalence between `C` and `ULiftHom C`.  -/
CategoryTheory.ULiftHom.equiv : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → C ≌ CategoryTheory.ULiftHom C
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- (Implementation.) Any cone over `cospan f g` indeed factors through the constructed cone.
 -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : AlgebraicGeometry.PresheafedSpace C} →
      (f : X ⟶ Z) →
        [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] →
          (g : Y ⟶ Z) →
            (s : CategoryTheory.Limits.PullbackCone f g) →
              s.pt ⟶ (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f g).pt
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.mergeWith!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (mergeFn : (a : α) → β a → β a → β a)
  (t₁ t₂ : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.mergeWith! mergeFn t₁ t₂ =
    Std.DTreeMap.Internal.Impl.foldl
      (fun t a b₂ =>
        Std.DTreeMap.Internal.Impl.alter! a
          (fun x =>
            match x with
            | none => some b₂
            | some b₁ => some (mergeFn a b₁ b₂))
          t)
      t₁ t₂