mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.Methods.mk.inj : ∀ {initLB initUB : Lean.Expr → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr)}
  {proveLE proveLT : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr}
  {roundUp roundDown : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr}
  {eval : Lean.Expr → Lean.MetaM (ℤ × Lean.Expr × Lean.Expr)} {mkNumeral : ℤ → Lean.MetaM Lean.Expr}
  {initLB_1 initUB_1 : Lean.Expr → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr)}
  {proveLE_1 proveLT_1 : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr}
  {roundUp_1 roundDown_1 : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr}
  {eval_1 : Lean.Expr → Lean.MetaM (ℤ × Lean.Expr × Lean.Expr)} {mkNumeral_1 : ℤ → Lean.MetaM Lean.Expr},
  { initLB := initLB, initUB := initUB, proveLE := proveLE, proveLT := proveLT, roundUp := roundUp,
        roundDown := roundDown, eval := eval, mkNumeral := mkNumeral } =
      { initLB := initLB_1, initUB := initUB_1, proveLE := proveLE_1, proveLT := proveLT_1, roundUp := roundUp_1,
        roundDown := roundDown_1, eval := eval_1, mkNumeral := mkNumeral_1 } →
    initLB = initLB_1 ∧
      initUB = initUB_1 ∧
        proveLE = proveLE_1 ∧
          proveLT = proveLT_1 ∧ roundUp = roundUp_1 ∧ roundDown = roundDown_1 ∧ eval = eval_1 ∧ mkNumeral = mkNumeral_1
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_vadd_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v w : V) (p q : P),
  ((signedDist v) (w +ᵥ p)) q = -inner ℝ (NormedSpace.normalize v) w + ((signedDist v) p) q
-- Lean.Linter.Init
Lean.Linter.LinterOptions.mk.sizeOf_spec : ∀ (toOptions : Lean.Options) (linterSets : Lean.Linter.LinterSets),
  sizeOf { toOptions := toOptions, linterSets := linterSets } = 1 + sizeOf toOptions + sizeOf linterSets
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get!_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂).get! k = if k ∈ m₂ then m₁.get! k else default
-- Std.Http.Data.URI.Basic
/-- Finds all values of a query parameter by key name. Returns an empty array if the key is not found.
The values remain encoded as `EncodedQueryParam`.
 -/
Std.Http.URI.Query.findAllEncoded : Std.Http.URI.Query → Std.Http.URI.EncodedQueryParam → Array (Option Std.Http.URI.EncodedQueryParam)
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U),
  U.fromSpecStalkOfMem x hxU = U.fromSpecStalkOfMem x hxU
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.mk : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            (obj : C) →
              (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj) →
                autoParam (CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0)
                    CategoryTheory.DifferentialObject.d_squared._autoParam →
                  CategoryTheory.DifferentialObject S C
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.le_maxKey!_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t.contains k = true → (cmp k t.maxKey!).isLE = true
-- Lean.Data.Lsp.CodeActions
/-- The client supports code action literals as a valid response of the `textDocument/codeAction` request.  -/
Lean.Lsp.CodeActionClientCapabilities.codeActionLiteralSupport? : Lean.Lsp.CodeActionClientCapabilities → Option Lean.Lsp.CodeActionLiteralSupport
-- Mathlib.Logic.Equiv.List
/-- A listable type with decidable equality is encodable.  -/
Encodable.encodableOfList : {α : Type u_1} → [DecidableEq α] → (l : List α) → (∀ (x : α), x ∈ l) → Encodable α
-- Mathlib.RingTheory.SimpleModule.Basic
instIsSimpleModule : ∀ (R : Type u_5) [inst : DivisionRing R], IsSimpleModule R R
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toLinearMap_apply : ∀ {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₂) (x : A₁), e.toLinearMap x = e x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.div : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) [Lean.Grind.NoNatZeroDivisors α]
  (p₁ : Lean.Grind.CommRing.Poly) (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.div_cert p₁ k p = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 → Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.filter.eq_1 : ∀ {α β : Type w} [inst : Std.Iterator α Id β] (f : β → Bool) (it : Std.Iter β),
  Std.Iter.filter f it = (Std.IterM.filter f it.toIterM).toIter
-- Init.Data.Array.Lemmas
Array.contains.eq_1 : ∀ {α : Type u} [inst : BEq α] (as : Array α) (a : α), as.contains a = as.any fun x => a == x
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal mono category is a category in which every monomorphism is normal.  -/
CategoryTheory.IsNormalMonoCategory.normalMonoOfMono : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  [self : CategoryTheory.IsNormalMonoCategory C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f],
  Nonempty (CategoryTheory.NormalMono f)
-- Std.Data.DTreeMap.Raw.Basic
/-- Partitions a tree map into two tree maps based on a predicate.  -/
Std.DTreeMap.Raw.partition : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      ((a : α) → β a → Bool) → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α β cmp × Std.DTreeMap.Raw α β cmp
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.instCategory : CategoryTheory.Category.{u, u + 1} Semigrp
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.smulCommClass' : ∀ {R : Type u_3} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided] {α : Type u_5} [inst_2 : SMul α R]
  [inst_3 : IsScalarTower α R R] [SMulCommClass R α R], SMulCommClass (R ⧸ I) α (R ⧸ I)
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.commute_iff : ∀ {α : Type u_1} {n : Type u_4} [inst : NonUnitalSemiring α] [inst_1 : StarRing α] [inst_2 : Fintype n]
  {A B : Matrix n n α}, A.IsHermitian → B.IsHermitian → (Commute A B ↔ (A * B).IsHermitian)
-- Aesop.Builder.Basic
Aesop.RuleBuilderInput.options : Aesop.RuleBuilderInput → Aesop.RuleBuilderOptions
-- Init.Notation
/-- `a % b` computes the remainder upon dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For `Nat` and `Int` it satisfies `a % b + b * (a / b) = a`,
  and `a % 0` is defined to be `a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `%` in identifiers is `mod`. -/
«term_%_» : Lean.TrailingParserDescr
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.mk.sizeOf_spec : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] (set : Lean.PersistentHashMap α Unit),
  sizeOf { set := set } = 1 + sizeOf set
-- Mathlib.Data.Nat.Factorization.Defs
/-- The equiv between `ℕ+` and `ℕ →₀ ℕ` with support in the primes.  -/
Nat.factorizationEquiv : ℕ+ ≃ { f // ∀ p ∈ f.support, Nat.Prime p }
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_mul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f g : α → ENNReal},
  Measurable f → Measurable g → μ.withDensity (f * g) = (μ.withDensity f).withDensity g
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
HasCompactSupport.toSchwartzMap_toFun : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} (h₁ : HasCompactSupport f) (h₂ : ContDiff ℝ (↑⊤) f) (a : E),
  (h₁.toSchwartzMap h₂) a = f a
-- Mathlib.Data.TypeVec
TypeVec.appendFun_comp_splitFun : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {γ : TypeVec.{u_2} n} {β : Type u_1} {δ : Type u_2} {ε : TypeVec.{u_3} (n + 1)}
  (f₀ : ε.drop.Arrow α) (f₁ : α.Arrow γ) (g₀ : ε.last → β) (g₁ : β → δ),
  TypeVec.comp (f₁ ::: g₁) (TypeVec.splitFun f₀ g₀) = TypeVec.splitFun (TypeVec.comp f₁ f₀) (g₁ ∘ g₀)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The universal property of the localization for the constructed localized category
when there is a left calculus of fractions.  -/
CategoryTheory.MorphismProperty.LeftFraction.Localization.strictUniversalPropertyFixedTarget : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W : CategoryTheory.MorphismProperty C) →
      [inst_1 : W.HasLeftCalculusOfFractions] →
        (E : Type u_4) →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} E] →
            CategoryTheory.Localization.StrictUniversalPropertyFixedTarget
              (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) W E
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.toList.congr_simp : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α] (r r_1 : Std.Rco α),
  r = r_1 → r.toList = r_1.toList
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_insertEntryIfNew_le_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k}, (compare (Std.Internal.List.minKey (Std.Internal.List.insertEntryIfNew k v l) ⋯) k).isLE = true
-- Init.Data.String.Search
/-- Returns the last character in `s`. If `s` is empty, returns `none`.

Examples:

* `"abc".back? = some 'c'`

* `"".back? = none`
 -/
String.back? : String → Option Char
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instAddZeroClass : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → AddZeroClass (E →ₛₗ.[σ] F)
-- Std.Data.TreeMap.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.TreeMap.toList : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → List (α × β)
-- Mathlib.LinearAlgebra.Matrix.Rank
Finset.equivFinOfCardEq.congr_simp : ∀ {α : Type u_1} {s : Finset α} {n : ℕ} (h : s.card = n), Finset.equivFinOfCardEq h = Finset.equivFinOfCardEq h
-- Mathlib.RingTheory.Unramified.Locus
Algebra.isUnramifiedIn_top : ∀ {R : Type u_1} [inst : CommRing R] (A : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.IsUnramifiedIn A ⊤
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
/-- Canonical inclusion of `M` into the symmetric algebra `SymmetricAlgebra R M`.  -/
SymmetricAlgebra.ι : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] SymmetricAlgebra R M
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.mk.injEq : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x : ↥X) (y : ↥Y) (s : ↥S) (hx : f x = s) (hy : g y = s)
  (x_1 : ↥X) (y_1 : ↥Y) (s_1 : ↥S) (hx_1 : f x_1 = s_1) (hy_1 : g y_1 = s_1),
  ({ x := x, y := y, s := s, hx := hx, hy := hy } = { x := x_1, y := y_1, s := s_1, hx := hx_1, hy := hy_1 }) =
    (x = x_1 ∧ y = y_1 ∧ s = s_1)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.of_uncurry_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] {x : MeasurableSpace α}
  {x_1 : MeasurableSpace γ} {f : α → γ → β},
  MeasureTheory.StronglyMeasurable (Function.uncurry f) → ∀ {x : α}, MeasureTheory.StronglyMeasurable (f x)
-- Mathlib.RingTheory.Ideal.Nonunits
exists_max_ideal_of_mem_nonunits : ∀ {α : Type u_2} {a : α} [inst : CommSemiring α], a ∈ nonunits α → ∃ I, I.IsMaximal ∧ a ∈ I
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.parseRes : Std.Internal.Parsec.ByteArray.Parser (ℕ × Array ℕ)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.comp.eq_2 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.WithInitial C) (_X : C),
  CategoryTheory.WithInitial.comp = fun _f _g => PUnit.unit
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_right_inj : ∀ {x y z : ℝ}, 0 < x → x ≠ 1 → (x ^ y = x ^ z ↔ y = z)
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Frame.toCompleteLattice : {α : Type u_1} → [self : Order.Frame α] → CompleteLattice α
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_ofNatIsoRight_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G H : CategoryTheory.Functor D C} (adj : F ⊣ G) (iso : G ≅ H) {X : C} {Y : D}
  (f : F.obj X ⟶ Y),
  ((adj.ofNatIsoRight iso).homEquiv X Y) f = CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y) f) (iso.hom.app Y)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.toBackwardSearcher_eq : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice},
  String.Slice.Pattern.ToBackwardSearcher.toSearcher p s =
    String.Slice.Pattern.ToBackwardSearcher.toSearcher (fun x => decide (p x)) s
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
continuous_of_linear_of_boundₛₗ : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : Ring 𝕜₂]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜₂ F]
  {σ : 𝕜 →+* 𝕜₂} {f : E → F},
  (∀ (x y : E), f (x + y) = f x + f y) →
    (∀ (c : 𝕜) (x : E), f (c • x) = σ c • f x) → ∀ {C : ℝ}, (∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → Continuous f
-- Mathlib.GroupTheory.Nilpotent
instCommGroupOfIsSimpleGroupOfIsNilpotent : {G : Type u_1} → [inst : Group G] → [IsSimpleGroup G] → [Group.IsNilpotent G] → CommGroup G
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₁₀_single_one : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₁₀ A)) fun₀ | 1 => a) = 0
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofReal_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ENNReal.ofReal (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a lattice
with possibly different definitional equalities.  -/
Lattice.copy : {α : Type u} →
  (c : Lattice α) →
    (le : α → α → Prop) → le = LE.le → (sup : α → α → α) → sup = max → (inf : α → α → α) → inf = min → Lattice α
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.instReflectsIsomorphismsMonadFunctorMonadToFunctor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.monadToFunctor C).ReflectsIsomorphisms
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis'.eq_of_subset_indep : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis' I X → M.Indep J → I ⊆ J → J ⊆ X → I = J
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.instReflectiveFunctorOppositeSheafSheafToPresheafOfHasWeakSheafify : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          [CategoryTheory.HasWeakSheafify J A] → CategoryTheory.Reflective (CategoryTheory.sheafToPresheaf J A)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- A continuous linear operator is self-adjoint iff it is equal to its adjoint.  -/
ContinuousLinearMap.isSelfAdjoint_iff' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {A : E →L[𝕜] E}, IsSelfAdjoint A ↔ ContinuousLinearMap.adjoint A = A
-- Init.Data.List.Lemmas
List.getElem?_filter : ∀ {α : Type u_1} {a : α} {xs : List α} {p : α → Bool} {i : ℕ},
  i < (List.filter p xs).length → (List.filter p xs)[i]? = some a → p a = true
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instCategory.eq_1 : GrpCat.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := MonoidHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @GrpCat.instCategory._proof_1,
    comp_id := @GrpCat.instCategory._proof_2, assoc := @GrpCat.instCategory._proof_3 }
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_zero : ∀ {S : Type u_5} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Semiring R] (abv : R → S)
  [IsAbsoluteValue abv], abv 0 = 0
-- Mathlib.InformationTheory.Hamming
Hamming.toHamming_add : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → Add (β i)] {x y : (i : ι) → β i},
  Hamming.toHamming (x + y) = Hamming.toHamming x + Hamming.toHamming y
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- This left homology map data expresses compatibilities of the left homology data
constructed by `LeftHomologyData.ofEpiOfIsIsoOfMono`  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h : S₁.LeftHomologyData) →
            [inst_2 : CategoryTheory.Epi φ.τ₁] →
              [inst_3 : CategoryTheory.IsIso φ.τ₂] →
                [inst_4 : CategoryTheory.Mono φ.τ₃] →
                  CategoryTheory.ShortComplex.LeftHomologyMapData φ h
                    (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.mkHom.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  {s t : CategoryTheory.Limits.Cofork f g} (k k_1 : s.pt ⟶ t.pt) (e_k : k = k_1)
  (w : CategoryTheory.CategoryStruct.comp s.π k = t.π),
  CategoryTheory.Limits.Cofork.mkHom k w = CategoryTheory.Limits.Cofork.mkHom k_1 ⋯
-- Mathlib.Algebra.Lie.InvariantForm
LieAlgebra.InvariantForm.orthogonal_isCompl : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L] [Module.Finite K L]
  (Φ : LinearMap.BilinForm K L),
  Φ.Nondegenerate →
    ∀ (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ),
      Φ.IsRefl →
        (∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I) →
          ∀ (I : LieIdeal K L), IsAtom I → IsCompl I (LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv I)
-- Mathlib.Algebra.Group.ULift
ULift.addLeftCancelMonoid.eq_1 : ∀ {α : Type u} [inst : AddLeftCancelMonoid α],
  ULift.addLeftCancelMonoid = Function.Injective.addLeftCancelMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯
-- Lean.Parser.Do
Lean.Parser.Term.optMetaFalse : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.prodCongr_symm : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] {module_M : Module R M}
  {module_M₂ : Module R M₂} {module_M₃ : Module R M₃} {module_M₄ : Module R M₄} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄),
  (e₁.prodCongr e₂).symm = e₁.symm.prodCongr e₂.symm
-- Lean.Meta.ACLt
Lean.Meta.ACLt.ReduceMode.reduceSimpleOnly : Lean.Meta.ACLt.ReduceMode
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_eq_getValueD : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [instBEq : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α fun x => β} {fallback : β},
  t.Ordered → Std.DTreeMap.Internal.Impl.Const.getD t k fallback = Std.Internal.List.getValueD k t.toListModel fallback
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.sum_eq_of_subset : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] {p : SkewPolynomial R} (f : ℕ → R → S),
  (∀ (i : ℕ), f i 0 = 0) → ∀ {s : Finset ℕ}, p.support ⊆ s → p.sum f = ∑ n ∈ s, f n (p.coeff n)
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_setOfPred_re_le : ∀ (a : ℝ), frontier {z | z.re ≤ a} = {z | z.re = a}
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.brecOn.go : {motive_1 : Aesop.Script.StepTree → Sort u} →
  {motive_2 : Array Aesop.Script.StepTree → Sort u} →
    {motive_3 : List Aesop.Script.StepTree → Sort u} →
      (t : Aesop.Script.StepTree) →
        ((t : Aesop.Script.StepTree) → t.below → motive_1 t) →
          ((t : Array Aesop.Script.StepTree) → Aesop.Script.StepTree.below_1 t → motive_2 t) →
            ((t : List Aesop.Script.StepTree) → Aesop.Script.StepTree.below_2 t → motive_3 t) → motive_1 t ×' t.below
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
cfcL_integral : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [inst_6 : CompleteSpace A] [inst_7 : NormedSpace ℝ A] (a : A)
  (f : X → C(↑(spectrum 𝕜 a), 𝕜)),
  MeasureTheory.Integrable f μ →
    ∀ (ha : autoParam (p a) cfcL_integral._auto_1), ∫ (x : X), (cfcL ha) (f x) ∂μ = (cfcL ha) (∫ (x : X), f x ∂μ)
-- Mathlib.Algebra.Order.GroupWithZero.Lex
/-- Given linearly ordered groups with zero M, N, the natural projection ordered homomorphism from
`WithZero (Mˣ ×ₗ Nˣ)` to M, which is the linearly ordered group with zero that can be identified
as their product.  -/
LinearOrderedCommGroupWithZero.fst : (α : Type u_1) →
  (β : Type u_2) →
    [inst : LinearOrderedCommGroupWithZero α] →
      [inst_1 : LinearOrderedCommGroupWithZero β] → WithZero (Lex (αˣ × βˣ)) →*₀o α
-- Mathlib.Order.CompleteBooleanAlgebra
sdiff_eq_sInf : ∀ {α : Type u} [inst : Order.Coframe α] {a b : α}, a \ b = sInf {w | a ≤ b ⊔ w}
-- Mathlib.FieldTheory.Normal.Closure
/-- If `L/K/F` is a field tower where `L/F` is normal, then
`K` is normal over `F` if and only if `σ(K) = K` for every `σ ∈ K →ₐ[F] L`.  -/
IntermediateField.normal_iff_forall_fieldRange_eq : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [Normal F L]
  {K : IntermediateField F L}, Normal F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange = K
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H2π_eq_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x y : ↥(groupHomology.cycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H2π A)) x =
      (CategoryTheory.ConcreteCategory.hom (groupHomology.H2π A)) y ↔
    ↑x - ↑y ∈ groupHomology.boundaries₂ A
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.continuous_comp_right : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : AddMonoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (f : B →ₜ+ C),
  Continuous fun g => f.comp g
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A block containing `a` is the orbit of `a` under its stabilizer  -/
AddAction.IsBlock.orbit_stabilizer_eq : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X}
  [AddAction.IsPretransitive G X],
  AddAction.IsBlock G B → ∀ {a : X}, a ∈ B → AddAction.orbit (↥(AddAction.stabilizer G B)) a = B
-- Mathlib.Analysis.Complex.Norm
Complex.norm_add_le' : ∀ (z w : ℂ), ‖z + w‖ ≤ ‖z‖ + ‖w‖