mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Injective
/-- A dependent version of `ExtensionOf.ext`  -/
Module.Baer.ExtensionOf.dExt : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {a b : Module.Baer.ExtensionOf i f},
  a.domain = b.domain → (∀ ⦃x : ↥a.domain⦄ ⦃y : ↥b.domain⦄, ↑x = ↑y → ↑a.toLinearPMap x = ↑b.toLinearPMap y) → a = b
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.basicOpen_mul_le_right : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f g : A), ProjectiveSpectrum.basicOpen 𝒜 (f * g) ≤ ProjectiveSpectrum.basicOpen 𝒜 g
-- Mathlib.Topology.Algebra.Monoid
Submonoid.mem_nhds_one : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : CommMonoid M] (S : Submonoid M), IsOpen ↑S → ↑S ∈ nhds 1
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse_assoc : ∀ {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 D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] {Z : D}
  (h : e.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.counitInv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
      (CategoryTheory.CategoryStruct.comp (e.functor.map (CategoryTheory.Functor.OplaxMonoidal.η e.inverse)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε e.functor) h
-- Mathlib.Algebra.Regular.Basic
IsAddLeftRegular.add_left_eq_self_iff : ∀ {R : Type u_1} [inst : AddMonoid R] {a b : R}, IsAddLeftRegular a → (a + b = a ↔ b = 0)
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
/-- If `A →+* B` is flat and surjective on prime spectra, `B` is a faithfully flat `A`-algebra.  -/
Module.FaithfullyFlat.of_comap_surjective : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [Module.Flat A B],
  Function.Surjective (PrimeSpectrum.comap (algebraMap A B)) → Module.FaithfullyFlat A B
-- Mathlib.LinearAlgebra.Dimension.Finite
LinearIndependent.finset_card_le_finrank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] {b : Finset M}, (LinearIndependent R fun x => ↑x) → b.card ≤ Module.finrank R M
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α},
  List.find? (fun x_2 => x_2.1 == k) (Std.DHashMap.Const.toList m) = none ↔ m.contains k = false
-- Mathlib.Algebra.Ring.Parity
Nat.Odd.sub_odd : ∀ {m n : ℕ}, Odd m → Odd n → Even (m - n)
-- Mathlib.Tactic.Linarith.Datatypes
/-- `l.scale c` scales the values in `l` by `c` without modifying the order or keys.  -/
Mathlib.Tactic.Linarith.Linexp.scale : ℤ → Mathlib.Tactic.Linarith.Linexp → Mathlib.Tactic.Linarith.Linexp
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_mapM_map : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_8 : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → γ} {g : γ → n δ} {it : Std.IterM m β},
  (Std.IterM.mapM g (Std.IterM.map f it)).toList = (Std.IterM.mapM (fun b => g (f b)) it).toList
-- Lean.Server.Requests
Lean.Server.ServerRequestResponse.failure.inj : ∀ {α : Type} {code : Lean.JsonRpc.ErrorCode} {message : String} {code_1 : Lean.JsonRpc.ErrorCode} {message_1 : String},
  Lean.Server.ServerRequestResponse.failure code message = Lean.Server.ServerRequestResponse.failure code_1 message_1 →
    code = code_1 ∧ message = message_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- Two morphisms into a pullback are equal if their compositions with the pullback morphisms are
equal  -/
CategoryTheory.Limits.pullback.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {W : C} {k l : W ⟶ CategoryTheory.Limits.pullback f g},
  CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.pullback.fst f g) =
      CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.fst f g) →
    CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.pullback.snd f g) =
        CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.snd f g) →
      k = l
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_add_le_iff_right : ∀ {R : Type u} [inst : Semiring R] {n : ℕ} (p q : Polynomial R),
  p.natDegree ≤ n → ((p + q).natDegree ≤ n ↔ q.natDegree ≤ n)
-- Mathlib.LinearAlgebra.Matrix.Permutation
Matrix.conjTranspose_permMatrix : ∀ {n : Type u_1} {R : Type u_2} [inst : DecidableEq n] (σ : Equiv.Perm n) [inst_1 : NonAssocSemiring R]
  [inst_2 : StarRing R], (Equiv.Perm.permMatrix R σ).conjTranspose = Equiv.Perm.permMatrix R σ⁻¹
-- Aesop.RuleTac.Basic
/-- A `RuleTac` is the tactic that is run when a rule is applied to a goal.
 -/
Aesop.RuleTac : Type
-- Mathlib.Data.Setoid.Basic
Setoid.ker_eq_bot_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Setoid.ker f = ⊥ ↔ Function.Injective f
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- Bundled version of lax braided functors.  -/
CategoryTheory.LaxBraidedFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        (D : Type u₂) →
          [inst : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_2 : CategoryTheory.MonoidalCategory D] →
              [CategoryTheory.BraidedCategory D] → Type (max (max (max u₁ u₂) v₁) v₂)
-- Std.Data.ExtHashMap.Lemmas
/-- Simpler variant of `getD_filter` when `LawfulBEq` is available.  -/
Std.ExtHashMap.getD_filter' : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  {f : α → β → Bool} {k : α} {fallback : β},
  (Std.ExtHashMap.filter f m).getD k fallback = (Option.filter (f k) m[k]?).getD fallback
-- Init.Data.UInt.Bitwise
UInt64.zero_or : ∀ {a : UInt64}, 0 ||| a = a
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
BirdDet.sumFrom_stop : ∀ {R : Type u_1} [inst : CommRing R] (n lo : ℕ) (f : ℕ → R), ¬lo < n → BirdDet.sumFrom n lo f = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.mk : {J : CategoryTheory.Limits.MultispanShape} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (left : J.L → C) →
        (right : J.R → C) →
          ((a : J.L) → left a ⟶ right (J.fst a)) →
            ((a : J.L) → left a ⟶ right (J.snd a)) → CategoryTheory.Limits.MultispanIndex J C
-- Mathlib.Data.Set.Image
/-- **Alias** of `Set.image_compl_eq_range_sdiff_image`. -/
Set.image_compl_eq_range_diff_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set α), f '' sᶜ = Set.range f \ f '' s
-- Init.Data.Vector.Basic
/-- Note that the universe level is constrained to `Type` here,
to avoid having to have the predicate live in `p : α → m (ULift Bool)`.
 -/
Vector.findRevM? : {n : ℕ} → {α : Type} → {m : Type → Type} → [Monad m] → (α → m Bool) → Vector α n → m (Option α)
-- Init.Data.String.Basic
String.Pos.get.congr_simp : ∀ {s : String} (pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : pos ≠ s.endPos), pos.get h = pos_1.get ⋯
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.posFittingComp.eq_1 : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L], LieModule.posFittingComp R L M = ⨆ x, LieModule.posFittingCompOf R M x
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
/-- The Laplacian matrix is positive semidefinite  -/
SimpleGraph.posSemidef_lapMatrix : ∀ {V : Type u_1} (R : Type u_2) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : Field R] [inst_4 : LinearOrder R] [IsStrictOrderedRing R] [inst_6 : StarRing R]
  [TrivialStar R], (SimpleGraph.lapMatrix R G).PosSemidef
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.mk : {α : Type u_4} →
  {β : Type u_5} →
    [inst : UniformSpace α] →
      [inst_1 : UniformSpace β] →
        (toEquiv : α ≃ β) → UniformContinuous toEquiv.toFun → UniformContinuous toEquiv.invFun → α ≃ᵤ β
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} {f : β → β}, m.WF → (m.modify k f).isEmpty = m.isEmpty
-- Mathlib.GroupTheory.Congruence.Defs
Con.mulOneClass.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] (c : Con M),
  c.mulOneClass = { toOne := c.one, toMul := c.hasMul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.FieldTheory.AlgebraicClosure
/-- The algebraic closure in `E` of the algebraic closure of `F` in `E` is equal to itself.  -/
algebraicClosure.algebraicClosure_eq_bot : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  algebraicClosure (↥(algebraicClosure F E)) E = ⊥
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.mem_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ {k : α}, k ∈ t₁ ↔ k ∈ t₂
-- Mathlib.Topology.Separation.Hausdorff
lim_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] (x : X), (nhds x).lim = x
-- Mathlib.Algebra.BigOperators.Finprod
AddMonoidHom.map_finsum_plift : ∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (f : M →+ N)
  (g : α → M), Function.HasFiniteSupport (g ∘ PLift.down) → f (∑ᶠ (x : α), g x) = ∑ᶠ (x : α), f (g x)
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.map_apply_of : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] {G' : ι → Type u_5}
  [inst_3 : (i : ι) → AddCommMonoid (G' i)] {f' : (i j : ι) → i ≤ j → G' i →+ G' j} (g : (i : ι) → G i →+ G' i)
  (hg : ∀ (i j : ι) (h : i ≤ j), (g j).comp (f i j h) = (f' i j h).comp (g i)) {i : ι} (x : G i),
  (AddCommGroup.DirectLimit.map g hg) ((AddCommGroup.DirectLimit.of G f i) x) =
    (AddCommGroup.DirectLimit.of G' f' i) ((g i) x)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- An alias of `ContinuousMultilinearMap.normedAddCommGroup` with non-dependent types to help
typeclass search.  -/
ContinuousMultilinearMap.normedAddCommGroup' : {𝕜 : Type u} →
  {ι : Type v} →
    {G : Type wG} →
      {G' : Type wG'} →
        [Fintype ι] →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup G] →
              [inst_2 : NormedSpace 𝕜 G] →
                [inst_3 : SeminormedAddCommGroup G'] →
                  [inst_4 : NormedSpace 𝕜 G'] → NormedAddCommGroup (ContinuousMultilinearMap 𝕜 (fun x => G') G)
-- Mathlib.Data.Matrix.Basic
AddMonoidHom.mapMatrix_neg : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [inst : AddZeroClass α] [inst_1 : AddCommGroup β]
  (f : α →+ β), (-f).mapMatrix = -f.mapMatrix
-- Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
eventuallyMeasurableSingleton : ∀ {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [inst : CountableInterFilter l] [MeasurableSingletonClass α],
  MeasurableSingletonClass α
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.denom.eq_1 : ∀ {K : Type u} [inst : Field K] (x : RatFunc K), x.denom = x.numDenom.2
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.mulVec_conjTranspose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype m] [inst_2 : StarRing α]
  (A : Matrix m n α) (x : m → α), A.conjTranspose.mulVec x = star (Matrix.vecMul (star x) A)
-- Mathlib.ModelTheory.Syntax
/-- The implication between two bounded formulas.  -/
FirstOrder.«term_⟹_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.le_colimitsOfShape_punit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  W ≤ W.colimitsOfShape (CategoryTheory.Discrete PUnit.{w + 1})
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_isBasis_iff' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {M : Matroid α} {I X : Set β} {hf : Set.InjOn f M.E},
  (M.map f hf).IsBasis I X ↔ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.homMk_surjective : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {S : T} {X Y : CategoryTheory.Over S} (f : X ⟶ Y),
  ∃ g, ∃ (hg : CategoryTheory.CategoryStruct.comp g Y.hom = X.hom), f = CategoryTheory.Over.homMk g ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → (Std.DTreeMap.Const.unitOfList l cmp).getKeyD k' fallback = k
-- Init.Data.Fin.Basic
/-- The successor, with an increased bound.

This differs from adding `1`, which instead wraps around.

Examples:
* `(2 : Fin 3).succ = (3 : Fin 4)`
* `(2 : Fin 3) + 1 = (0 : Fin 3)`
 -/
Fin.succ : {n : ℕ} → Fin n → Fin (n + 1)
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.inner : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → Std.Iterators.Types.StepSizeIterator α m β → Std.IterM m β
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.op_vadd_finset_add_eq_add_vadd_finset : ∀ {α : Type u_2} [inst : AddSemigroup α] [inst_1 : DecidableEq α] (a : α) (s t : Finset α),
  (AddOpposite.op a +ᵥ s) + t = s + (a +ᵥ t)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fract_add_ZSpan : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (m : E) {v : E},
  v ∈ Submodule.span ℤ (Set.range ⇑b) → ZSpan.fract b (m + v) = ZSpan.fract b m
-- Aesop.Forward.State
/-- Add multiple pattern substitutions to the forward state.  -/
Aesop.ForwardState.enqueuePatSubsts : Aesop.PatSubstSource → Array (Aesop.ForwardRule × Aesop.Substitution) → Aesop.ForwardState → Aesop.ForwardState
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getCharValue? : Lean.Expr → OptionT Id Char
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1`, `μ` is nonarchimedean, and `x` is multiplicative for `μ`, then `x` is
multiplicative for `smoothingSeminorm`.  -/
smoothingSeminorm_of_mul : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean ⇑μ) {x : R},
  (∀ (y : R), μ (x * y) = μ x * μ y) →
    ∀ (y : R), (smoothingSeminorm μ hμ1 hna) (x * y) = (smoothingSeminorm μ hμ1 hna) x * (smoothingSeminorm μ hμ1 hna) y
-- Mathlib.Analysis.Normed.Affine.Simplex
Affine.Simplex.Scalene.eq_1 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : Module R V] [inst_4 : NormedAddTorsor V P] {n : ℕ}
  (s : Affine.Simplex R P n), s.Scalene = Function.Injective fun i => dist (s.points (↑i).1) (s.points (↑i).2)
-- Mathlib.Data.Fin.SuccPred
/-- While in many cases `finCongr` is better than `Equiv.cast`/`cast`, sometimes we want to apply
a generic theorem about `cast`.  -/
finCongr_eq_equivCast : ∀ {n m : ℕ} (h : n = m), finCongr h = Equiv.cast ⋯
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The elements of `A.nonunits` are those of the maximal ideal of `A`.

See also `coe_mem_nonunits_iff`, which has a simpler right-hand side but requires the element
to be in `A` already.
 -/
ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal : ∀ {K : Type u} [inst : Field K] {A : ValuationSubring K} {a : K},
  a ∈ A.nonunits ↔ ∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ IsLocalRing.maximalIdeal ↥A
-- Mathlib.GroupTheory.Coset.Defs
/-- The equivalence relation corresponding to the partition of a group by right cosets
of a subgroup.  -/
QuotientAddGroup.rightRel : {α : Type u_1} → [inst : AddGroup α] → AddSubgroup α → Setoid α
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.mulLeft.congr_simp : ∀ (R : Type u_14) {A : Type u_15} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (a a_1 : A), a = a_1 → LinearMap.mulLeft R a = LinearMap.mulLeft R a_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The first projection of a binary fan.  -/
CategoryTheory.Limits.BinaryFan.fst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (s : CategoryTheory.Limits.BinaryFan X Y) →
        ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj
            { as := CategoryTheory.Limits.WalkingPair.left } ⟶
          (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_at_intCast : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {S : Type u_1} [inst_1 : Ring S] (f : R →+* S) (n : ℤ),
  Polynomial.eval₂ f (↑n) p = f (Polynomial.eval (↑n) p)
-- Mathlib.Order.SymmDiff
bihimp_isAssociative : ∀ {α : Type u_2} [inst : BooleanAlgebra α], Std.Associative fun x1 x2 => bihimp x1 x2
-- Mathlib.Data.Multiset.Bind
Multiset.coe_bind : ∀ {α : Type u_1} {β : Type v} (l : List α) (f : α → List β), ((↑l).bind fun a => ↑(f a)) = ↑(List.flatMap f l)
-- Std.Http.Data.Status
Std.Http.Status.instToString : ToString Std.Http.Status
-- Init.Data.SInt.Lemmas
Int16.toBitVec_mod : ∀ {a b : Int16}, (a % b).toBitVec = a.toBitVec.srem b.toBitVec
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_of_mem_closedBall' : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a b : E} {r : ℝ}, b ∈ Metric.closedBall a r → ‖b‖ ≤ ‖a‖ + r
-- Mathlib.SetTheory.ZFC.VonNeumann
/-- The von Neumann hierarchy is defined so that `V_ o` is the union of the powersets of all
`V_ a` for `a < o`. It satisfies the following properties:

- `vonNeumann_zero`: `V_ 0 = ∅`
- `vonNeumann_add_one`: `V_ (a + 1) = powerset (V_ a)`
- `vonNeumann_of_isSuccPrelimit`: `IsSuccPrelimit a → V_ a = ⋃ b < a, V_ b`
 -/
ZFSet.vonNeumann : Ordinal.{u} → ZFSet.{u}
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.add_mem_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A} {r s : R},
  r + s ∈ spectrum R a ↔ r ∈ spectrum R (-(algebraMap R A) s + a)
-- Mathlib.Topology.Maps.Basic
IsOpenMap.isOpen_range : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → IsOpen (Set.range f)
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.sub_cons : ∀ {α : Type u_1} {n : ℕ} [inst : Sub α] (v : Fin n.succ → α) (y : α) (w : Fin n → α),
  v - Matrix.vecCons y w = Matrix.vecCons (Matrix.vecHead v - y) (Matrix.vecTail v - w)
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsKolmogorovProcess.measurablePair : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {X : T → Ω → E} {P : MeasureTheory.Measure Ω} {p q : ℝ} {M : NNReal},
  ProbabilityTheory.IsKolmogorovProcess X P p q M → ∀ (s t : T), Measurable fun ω => (X s ω, X t ω)
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_le_of_apply_getElem_le_apply_maxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β}
  {xs : List α} (h : xs ≠ []) {k : ℕ} (hi : k < xs.length), f (List.maxOn f xs h) ≤ f xs[k] → List.maxIdxOn f xs h ≤ k
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_inter_eq_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∈ t₂) → (t₁ ∩ t₂).size = t₁.size
-- Mathlib.RingTheory.IdealFilter.Basic
IdealFilter.IsGabriel.toIsUniform : ∀ {A : Type u_1} {inst : Ring A} {F : IdealFilter A} [self : F.IsGabriel], F.IsUniform
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- The image of the unit ball under a continuous alternating map is bounded.  -/
ContinuousAlternatingMap.unit_le_opNorm : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] {m : ι → E} (f : E [⋀^ι]→L[𝕜] F), ‖m‖ ≤ 1 → ‖f m‖ ≤ ‖f‖
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rci.Internal.toList_eq_toList_iter : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rci α}, r.toList = (Std.Rci.Internal.iter r).toList
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.emphLike.opener : Char → String → String → (Lean.Doc.Parser.InlineCtxt → Option ℕ) → Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserFn
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.counit_domCongr : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (e : M ≃* N) (x : MonoidAlgebra A M),
  CoalgebraStruct.counit ((MonoidAlgebra.domCongr R A e) x) = CoalgebraStruct.counit x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : β k → β k},
  (t.modify k f).get? k' = if h : cmp k k' = Ordering.eq then cast ⋯ (Option.map f (t.get? k)) else t.get? k'
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_roc_eq_none : ∀ {m n : ℤ} {i : ℕ}, (n - m).toNat ≤ i → (m<...=n).toArray[i]? = none
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.op_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  P.isoClosure.op = P.op.isoClosure
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
exists_lt_add_iff_lt_right : ∀ {α : Type u_1} [inst : LinearOrder α] {P : α → Prop} {b c : α} [inst_1 : AddCommMagma α] [CanonicallyOrderedAdd α]
  [AddLeftReflectLT α] [IsLeftCancelAdd α], (∃ a < b + c, P a) ↔ (∃ a < c, P a) ∨ ∃ d < b, P (d + c)
-- Lean.Parser.Basic
Lean.Parser.fieldIdx : Lean.Parser.Parser
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.of_constToList_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp},
  (Std.DTreeMap.Const.toList t₁).Perm (Std.DTreeMap.Const.toList t₂) → t₁.Equiv t₂
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} [inst_2 : SizeOf C] (obj : C) (pt : (F.obj obj).obj)
  (isGalois :
    autoParam (CategoryTheory.PreGaloisCategory.IsGalois obj)
      CategoryTheory.PreGaloisCategory.PointedGaloisObject.isGalois._autoParam),
  sizeOf { obj := obj, pt := pt, isGalois := isGalois } = 1 + sizeOf obj + sizeOf pt + sizeOf isGalois
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_singleton : ∀ {α : Type u_2} [inst : Add α] {s : Set α} {b : α}, s + {b} = (fun x => x + b) '' s