mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂'_comp : ∀ {n : Type u_11} {m : Type u_12} {n' : Type u_13} {m' : Type u_14} {R : Type u_16} [inst : CommSemiring R]
  [inst_1 : Fintype n] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : DecidableEq m] [inst_5 : Fintype n']
  [inst_6 : Fintype m'] [inst_7 : DecidableEq n'] [inst_8 : DecidableEq m'] (M : Matrix n m R) (P : Matrix n n' R)
  (Q : Matrix m m' R),
  ((Matrix.toLinearMap₂' R) M).compl₁₂ (Matrix.toLin' P) (Matrix.toLin' Q) =
    (Matrix.toLinearMap₂' R) (P.transpose * M * Q)
-- Mathlib.Algebra.Module.Projective
/-- **Alias** of `Module.Projective.of_equiv`. -/
Module.Projective.of_ringEquiv : ∀ {R : Type u_8} {S : Type u_9} [inst : Semiring R] [inst_1 : Semiring S] {M : Type u_10} {N : Type u_11}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module S N] {σ : R →+* S}
  {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ] (e₂ : M ≃ₛₗ[σ] N)
  [Module.Projective R M], Module.Projective S N
-- Mathlib.ModelTheory.Basic
/-- Composition of first-order embeddings is associative.  -/
FirstOrder.Language.Embedding.comp_assoc : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] {Q : Type u_2} [inst_3 : L.Structure Q] (f : L.Embedding M N) (g : L.Embedding N P)
  (h : L.Embedding P Q), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.SMulMemClass.subtype_injective : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {A : Type u_1} [inst_2 : SetLike A M]
  [hA : SMulMemClass A R M] (S' : A), Function.Injective ⇑(SubMulAction.SMulMemClass.subtype S')
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.stalkMap.comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y Z : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (x : ↑↑X),
  AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (CategoryTheory.CategoryStruct.comp α β) x =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap β ((CategoryTheory.ConcreteCategory.hom α.base) x))
      (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x)
-- Lean.Meta.Tactic.Grind.Theorems
_private.Lean.Meta.Tactic.Grind.Theorems.0.Lean.Meta.Grind.Theorems.smap : {α : Type} → Lean.Meta.Grind.Theorems α → Lean.PHashMap Lean.Name (List α)
-- Lean.Parser.Term
Lean.Parser.Term.attrInstance.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.comp_α : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  CategoryTheory.CategoryStruct.comp f (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.α✝ f n) = 0
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.parseTransitionIndices : UInt32 → Std.Internal.Parsec.ByteArray.Parser (Array UInt8)
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.hasSum_repr : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (x : E), HasSum (fun i => ↑(b.repr x) i • b i) x
-- Mathlib.Topology.Algebra.Group.Basic
Pi.topologicalAddGroup : ∀ {β : Type v} {C : β → Type u_1} [inst : (b : β) → TopologicalSpace (C b)] [inst_1 : (b : β) → AddGroup (C b)]
  [∀ (b : β), IsTopologicalAddGroup (C b)], IsTopologicalAddGroup ((b : β) → C b)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_iff_forall_smul_nonpos`. -/
AntivaryOn.sub_smul_sub_nonpos : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β} {s : Set ι},
  AntivaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_subset_Ioo_union_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a a₁ b b₁ c d : α},
  a ≤ a₁ → c < b → b₁ ≤ d → Set.Ioo a₁ b₁ ⊆ Set.Ioo a b ∪ Set.Ioo c d
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.pretopology.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (P P_1 : CategoryTheory.MorphismProperty C) (e_P : P = P_1) [inst_2 : P.IsMultiplicative]
  [inst_3 : P.IsStableUnderBaseChange], P.pretopology = P_1.pretopology
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.isClopen_singleton_empty : ∀ {α : Type u_1} [inst : UniformSpace α], IsClopen {∅}
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.apply_one : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : DecidableEq R] [inst_2 : NoZeroDivisors R] [inst_3 : Nontrivial R]
  (x : R), 1 x = if x = 0 then 0 else 1
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.instInhabited : Inhabited CommSemiRingCat
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_associator_hom_snd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c d : B × C} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  (CategoryTheory.Bicategory.associator f g h).hom.2 = (CategoryTheory.Bicategory.associator f.2 g.2 h.2).hom
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b}, curveIntegralFun (-ω) γ = -curveIntegralFun ω γ
-- Init.Data.Nat.Fold
/-- Checks whether there is some number less that the given bound for which `f` returns `true`.

This is a tail-recursive equivalent of `Nat.any` that's used at runtime.

Examples:
* `Nat.anyTR 4 (fun i _ => i < 5) = true`
* `Nat.anyTR 7 (fun i _ => i < 5) = true`
* `Nat.anyTR 7 (fun i _ => i % 2 = 0) = true`
* `Nat.anyTR 1 (fun i _ => i % 2 = 1) = false`
 -/
Nat.anyTR : (n : ℕ) → ((i : ℕ) → i < n → Bool) → Bool
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert_support_idxOf : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} [inst : DecidableEq V] (p : G.Walk u v),
  w ∈ p.support → p.getVert (List.idxOf w p.support) = w
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go.match_1.eq_4 : ∀ {pu : Lean.Compiler.LCNF.Purity} (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1) (fvarId : Lean.FVarId) (idx : ℕ)
  (y : Lean.Compiler.LCNF.Arg pu) (h : pu = Lean.Compiler.LCNF.Purity.impure)
  (h_1 : (decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl))
  (h_2 :
    (decl : Lean.Compiler.LCNF.FunDecl pu) →
      (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h))
  (h_3 : (decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl))
  (h_4 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.Compiler.LCNF.Arg pu) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h))
  (h_5 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.FVarId) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h))
  (h_6 :
    (fvarId : Lean.FVarId) →
      (idx offset : ℕ) →
        (y : Lean.FVarId) →
          (ty : Lean.Expr) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h))
  (h_7 :
    (fvarId : Lean.FVarId) →
      (cidx : ℕ) →
        (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h))
  (h_8 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
            motive (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h))
  (h_9 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (objs? : Option ℕ) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h))
  (h_10 :
    (fvarId : Lean.FVarId) →
      (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.del fvarId h)),
  (match Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h with
    | Lean.Compiler.LCNF.CodeDecl.let decl => h_1 decl
    | Lean.Compiler.LCNF.CodeDecl.fun decl h => h_2 decl h
    | Lean.Compiler.LCNF.CodeDecl.jp decl => h_3 decl
    | Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h => h_4 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h => h_5 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h => h_6 fvarId idx offset y ty h
    | Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h => h_7 fvarId cidx h
    | Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h => h_8 fvarId n check persistent h
    | Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h => h_9 fvarId n check persistent objs? h
    | Lean.Compiler.LCNF.CodeDecl.del fvarId h => h_10 fvarId h) =
    h_4 fvarId idx y h
-- Mathlib.AlgebraicGeometry.Noetherian
/-- If `R` is a Noetherian ring, `Spec R` is a Noetherian topological space.  -/
AlgebraicGeometry.instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier : ∀ {R : CommRingCat} [IsNoetherianRing ↑R], TopologicalSpace.NoetherianSpace ↥(AlgebraicGeometry.Spec R)
-- Mathlib.MeasureTheory.Group.ModularCharacter
MeasureTheory.Measure.addModularCharacterFun.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : LocallyCompactSpace G] (g : G),
  MeasureTheory.Measure.addModularCharacterFun g =
    (MeasureTheory.Measure.map (fun x => x + g) MeasureTheory.Measure.addHaar).addHaarScalarFactor
      MeasureTheory.Measure.addHaar
-- Mathlib.Analysis.Fourier.ZMod
/-- The inverse Fourier transform on `ZMod N`.  -/
ZMod.«term𝓕⁻» : Lean.ParserDescr
-- Mathlib.CategoryTheory.EpiMono
/-- Every split mono whose retraction is mono is an iso.  -/
CategoryTheory.IsIso.of_mono_retraction' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (hf : CategoryTheory.SplitMono f)
  [CategoryTheory.Mono hf.retraction], CategoryTheory.IsIso f
-- Mathlib.Algebra.Order.Field.Basic
inv_strictAntiOn : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α],
  StrictAntiOn (fun x => x⁻¹) (Set.Ioi 0)
-- Mathlib.Analysis.Calculus.ContDiff.Convolution
/-- The derivative of the convolution `f * g` is given by `f * Dg`, when `f` is locally integrable
and `g` is `C^1` and compactly supported. Version where `g` depends on an additional parameter in an
open subset `s` of a parameter space `P` (and the compact support `k` is independent of the
parameter in `s`).  -/
MeasureTheory.hasFDerivAt_convolution_right_with_param : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} [inst_3 : RCLike 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F]
  [inst_8 : MeasurableSpace G] [inst_9 : NormedAddCommGroup G] [BorelSpace G] [inst_11 : NormedSpace 𝕜 G]
  [inst_12 : NormedAddCommGroup P] [inst_13 : NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F)
  {g : P → G → E'} {s : Set P} {k : Set G},
  IsOpen s →
    IsCompact k →
      (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
        MeasureTheory.LocallyIntegrable f μ →
          ContDiffOn 𝕜 1 (↿g) (s ×ˢ Set.univ) →
            ∀ (q₀ : P × G),
              q₀.1 ∈ s →
                HasFDerivAt (fun q => MeasureTheory.convolution f (g q.1) L μ q.2)
                  (MeasureTheory.convolution f (fun x => fderiv 𝕜 ↿g (q₀.1, x)) (ContinuousLinearMap.precompR (P × G) L)
                    μ q₀.2)
                  q₀
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {s₀ : E.I₀ → F.I₀} {h₀ : (i : E.I₀) → E.X i ⟶ F.X (s₀ i)}
  {w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i) (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreZeroHypercover.Hom.w₀._autoParam}
  {s₀_1 : E.I₀ → F.I₀} {h₀_1 : (i : E.I₀) → E.X i ⟶ F.X (s₀_1 i)}
  {w₀_1 :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀_1 i) (F.f (s₀_1 i)) = E.f i)
      CategoryTheory.PreZeroHypercover.Hom.w₀._autoParam},
  { s₀ := s₀, h₀ := h₀, w₀ := w₀ } = { s₀ := s₀_1, h₀ := h₀_1, w₀ := w₀_1 } → s₀ = s₀_1 ∧ h₀ ≍ h₀_1
-- Init.Meta.Defs
Lean.instQuoteProdMkStr1 : {α β : Type} → [Lean.Quote α] → [Lean.Quote β] → Lean.Quote (α × β)
-- Init.Data.List.Pairwise
List.pairwise_append : ∀ {α : Type u_1} {R : α → α → Prop} {l₁ l₂ : List α},
  List.Pairwise R (l₁ ++ l₂) ↔ List.Pairwise R l₁ ∧ List.Pairwise R l₂ ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, R a b
-- Mathlib.RingTheory.Adjoin.PowerBasis
Algebra.adjoin.powerBasis_gen : ∀ {K : Type u_1} {S : Type u_2} [inst : Field K] [inst_1 : CommRing S] [inst_2 : Algebra K S] {x : S}
  (hx : IsIntegral K x), (Algebra.adjoin.powerBasis hx).gen = ⟨x, ⋯⟩
-- Mathlib.Data.Stream.Init
Stream'.drop_append_stream : ∀ {α : Type u} (l : List α) (s : Stream' α), Stream'.drop l.length (l ++ₛ s) = s
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorAlgebra.toDirectSum_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  TensorAlgebra.toDirectSum ((TensorAlgebra.ι R) x) =
    (DirectSum.of (fun n => TensorPower R n M) 1) ((PiTensorProduct.tprod R) fun x_1 => x)
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.liftBoundedOrder.eq_1 : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder β] [inst_1 : Preorder α]
  [inst_2 : BoundedOrder α] (gi : GaloisCoinsertion u l),
  gi.liftBoundedOrder = { toOrderTop := ⋯.liftOrderTop, toOrderBot := gi.liftOrderBot }
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.IsExpansionOn.map_onRelation : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} {M : Type u_1} {inst : L.Structure M}
  {inst_1 : L'.Structure M} [self : ϕ.IsExpansionOn M] {n : ℕ} (R : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap (ϕ.onRelation R) x = FirstOrder.Language.Structure.RelMap R x
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
_private.Mathlib.Analysis.CStarAlgebra.CStarMatrix.0.CStarMatrix.lipschitzWith_toMatrixAux : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalCStarAlgebra A] [inst_3 : PartialOrder A] [inst_4 : StarOrderedRing A],
  LipschitzWith 1 ⇑CStarMatrix.ofMatrixₗ.symm
-- Mathlib.Data.Fin.Tuple.Curry
Function.FromTypes.uncurry_curry : ∀ {n : ℕ} {p : Fin n → Type u} {τ : Type u} (f : ((i : Fin n) → p i) → τ), (Function.FromTypes.curry f).uncurry = f
-- 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.termV_ : Lean.ParserDescr
-- Std.Async.Basic
/-- Runs all computations in an `Array` concurrently and returns all results as an array.
 -/
Std.Async.EAsync.concurrentlyAll : {ε α : Type} →
  Array (Std.Async.EAsync ε α) → optParam Task.Priority Task.Priority.default → Std.Async.EAsync ε (Array α)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.coeAddMonoidHom.eq_1 : ∀ {ι : Type u_1} {R : ι → Type u_2} {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → AddMonoid (R i)] [inst_2 : ∀ (i : ι), AddSubmonoidClass (S i) (R i)],
  RestrictedProduct.coeAddMonoidHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Nested additive monoid algebras can be taken in an arbitrary order.  -/
AddMonoidAlgebra.commRingEquiv : {R : Type u_3} →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : AddMonoid M] →
          [inst_2 : AddMonoid N] →
            AddMonoidAlgebra (AddMonoidAlgebra R M) N ≃+* AddMonoidAlgebra (AddMonoidAlgebra R N) M
-- Lean.Elab.Do.Control
_private.Lean.Elab.Do.Control.0.Lean.Elab.Do.synthUsingDefEq : String → Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Unit
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_subset_sdiff : ∀ {α : Type u_1} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂
-- Mathlib.ModelTheory.Basic
/-- The identity embedding from a structure to itself.  -/
FirstOrder.Language.Embedding.refl : (L : FirstOrder.Language) → (M : Type w) → [inst : L.Structure M] → L.Embedding M M
-- Mathlib.Algebra.Group.End
Equiv.Perm.one_def : ∀ {α : Type u_4}, 1 = Equiv.refl α
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_of_subset_left : ∀ {α : Type u_2} {s t u : Finset α}, s ⊆ u → Disjoint u t → Disjoint s t
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.continuousAt_iff' : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {b : β},
  ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhds b, dist (f x) (f b) < ε
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
SeparatingDual.mk : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : TopologicalSpace R] [inst_4 : Module R V], (∀ (x : V), x ≠ 0 → ∃ f, f x ≠ 0) → SeparatingDual R V
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep.match_1.splitter : (s : String.Slice) →
  (motive : String.Slice.Pattern.ForwardSliceSearcher s → Sort u_1) →
    (x : String.Slice.Pattern.ForwardSliceSearcher s) →
      ((pos : s.Pos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos)) →
        ((pos : s.Pos) → (h : pos ≠ s.endPos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h)) →
          ((needle : String.Slice) →
              (table : Vector ℕ needle.utf8ByteSize) →
                (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) →
                  (stackPos needlePos : String.Pos.Raw) →
                    (hn : needlePos < needle.rawEndPos) →
                      motive (String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn)) →
            (Unit → motive String.Slice.Pattern.ForwardSliceSearcher.atEnd) → motive x
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instBEqPolyCnstr.beq_spec : ∀ (x x_1 : Nat.Internal.Linear.PolyCnstr), (x == x_1) = (x.eq == x_1.eq && (x.lhs == x_1.lhs && x.rhs == x_1.rhs))
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.unop_op : ∀ {G : Type u_2} [inst : Group G] (S : Subgroup G), S.op.unop = S
-- Mathlib.Geometry.Manifold.Complex
/-- **Maximum modulus principle** on a connected set. Let `U` be a (pre)connected open set in a
complex normed space.  Let `f : E → F` be a function that is complex differentiable on `U`. Suppose
that `‖f x‖` takes its maximum value on `U` at `c ∈ U`. Then `f x = f c` for all `x ∈ U`.

TODO: change assumption from `IsMaxOn` to `IsLocalMax`.  -/
MDifferentiableOn.eqOn_of_isPreconnected_of_isMaxOn_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {H : Type u_3} [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless]
  {M : Type u_4} [inst_6 : TopologicalSpace M] [inst_7 : ChartedSpace H M] [IsManifold I 1 M] [StrictConvexSpace ℝ F]
  {f : M → F} {U : Set M} {c : M},
  MDiff[U] f → IsPreconnected U → IsOpen U → c ∈ U → IsMaxOn (norm ∘ f) U c → Set.EqOn f (Function.const M (f c)) U
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Certify the sign factor `(-1)^k` from `BirdDet.birdDet_eq`.  -/
Mathlib.Tactic.Determinant.certBirdSign : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} → ℕ → Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.sigmaFinite_bot_iff : ∀ {α : Type u_1} (μ : MeasureTheory.Measure α), MeasureTheory.SigmaFinite μ ↔ MeasureTheory.IsFiniteMeasure μ
-- Mathlib.RingTheory.SimpleModule.Isotypic
iSupIndep.linearEquiv.congr_simp : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Ring R] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] {p : ι → Submodule R N} (ind : iSupIndep p) (iSup_top : ⨆ i, p i = ⊤),
  ind.linearEquiv iSup_top = ind.linearEquiv iSup_top
-- Std.Http.Data.URI.Basic
/-- Returns the path segments as decoded strings.
Segments that cannot be decoded as UTF-8 are returned as their raw encoded form.
 -/
Std.Http.URI.Path.toDecodedSegments : Std.Http.URI.Path → Array String
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.contains : ∀ (c : Char) {s : Substring.Raw}, s.Valid → (Substring.Raw.Legacy.contains s c = true ↔ c ∈ s.toString.toList)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- ```
p = k₁*d.getPoly + k₂*m₂*c.p
```
The coefficient `k₁` is used because the leading monomial in `c` may not be monic.
Thus, if we follow the chain back to the input polynomial, we have that
`p = C * input_p` for a `C` that is equal to the product of all `k₁`s in the chain.
We have that `C ≠ 1` only if the ring does not implement `NoNatZeroDivisors`.
Here is a small example where we simplify `x+y` using the equations
`2*x - 1 = 0` (`c₁`), `3*y - 1 = 0` (`c₂`), and `6*z + 5 = 0` (`c₃`)
```
x + y + z            | s₁ := .input (x + y + z)
*2
=   - 1*1*(2*x - 1)
2*y + 2*z + 1        | s₂ := .step (2*y + 2*z + 1) 2 s₁ (-1) 1 c₁
*3
=   - 2*1*(3*y - 1)
6*z + 5              | s₃ := .step (6*z + 5) 3 s₂ (-2) 1 c₂
=   - 1*1*(6*z + 5)
0                    | s₄ := .step (0) 1 s₃ (-1) 1 c₃
```
For this chain, we build the certificate
```
(-3)*(2*x - 1) + (-2)*(3*y - 1) + (-1)*(6*z + 5)
```
for
```
0 = 6*(x + y + z)
```
Recall that if the ring implement `NoNatZeroDivisors`, then the following property holds:
```
∀ (k : Int) (a : α), k ≠ 0 → (intCast k) * a = 0 → a = 0
```
grind can deduce that `x+y+z = 0`
 -/
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.step : Lean.Grind.CommRing.Poly →
  ℤ →
    Lean.Meta.Grind.Arith.CommRing.PolyDerivation →
      ℤ →
        Lean.Grind.CommRing.Mon → Lean.Meta.Grind.Arith.CommRing.EqCnstr → Lean.Meta.Grind.Arith.CommRing.PolyDerivation
-- Mathlib.Data.NNRat.Lemmas
/-- A version of `NNRat.mul_den` without division.  -/
NNRat.den_mul_den_eq_den_mul_gcd : ∀ (q₁ q₂ : ℚ≥0), q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.unit_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : C} (f : X ⟶ Y) {Z : C} (h : e.inverse.obj (e.functor.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.unit.app X)
      (CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.unit.app Y) h)