mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_comp_of_ker_eq_bot : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {τ₁₂ : R →+* R₂}
  {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃},
  g.ker = ⊥ → (g ∘ₛₗ f).ker = f.ker
-- Batteries.Tactic.GeneralizeProofs
/-- Monad used to abstract proofs, to prepare for generalization.
Has a cache (of expr/type? pairs),
and it also has a reader context `Mathlib/Tactic/GeneralizeProofs/AContext.lean`
and a state `Mathlib/Tactic/GeneralizeProofs/AState.lean`.
 -/
Batteries.Tactic.GeneralizeProofs.MAbs : Type → Type
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.ext_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : TopologicalSpace.CompactOpens α}, s = t ↔ ↑s = ↑t
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Restrict.sigmaFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (s : Set α),
  MeasureTheory.SigmaFinite (μ.restrict s)
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_uint8 : ∀ (x : UInt8), ↑x = ↑x.toNat
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isIso_cyclesMap_of_iso : ∀ {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₂) [CategoryTheory.IsIso φ] [inst_3 : S₁.HasLeftHomology]
  [inst_4 : S₂.HasLeftHomology], CategoryTheory.IsIso (CategoryTheory.ShortComplex.cyclesMap φ)
-- Mathlib.Tactic.ClickSuggestions.Unfold
/-- Unfold a class projection if the instance is tagged with `@[default_instance]`.
This is used in the `unfold?` tactic in order to not show these unfolds to the user.
Similar to `Lean.Meta.unfoldProjInst?`.  -/
_private.Mathlib.Tactic.ClickSuggestions.Unfold.0.Mathlib.Tactic.ClickSuggestions.unfoldProjDefaultInst? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- Given a multilinear map `f` in `n` variables to the space of linear maps from `M (last n)` to
`M₂`, construct the corresponding multilinear map on `n+1` variables obtained by concatenating
the variables, given by `m ↦ f (init m) (m (last n))`  -/
MultilinearMap.uncurryRight : {R : Type uR} →
  {n : ℕ} →
    {M : Fin n.succ → Type v} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : Fin n.succ) → Module R (M i)] →
                [inst_4 : Module R M₂] →
                  MultilinearMap R (fun i => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂) → MultilinearMap R M M₂
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.eq_top_iff' : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H = ⊤ ↔ ∀ (x : G), x ∈ H
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.twoCochain_alt : ∀ {R : Type u_1} [inst : CommRing R] {L : Type u_2} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (a : ↥(LieModule.Cohomology.twoCochain R L M)) (x : L), (a x) x = 0
-- Init.Data.Order.Classes
Std.MinEqOr.mk : ∀ {α : Type u} [inst : Min α], (∀ (a b : α), a ⊓ b = a ∨ a ⊓ b = b) → Std.MinEqOr α
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of a product is the product of the trailing coefficients.
 -/
meromorphicTrailingCoeffAt_fun_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜} {x : 𝕜},
  (∀ σ ∈ s, MeromorphicAt (f σ) x) →
    meromorphicTrailingCoeffAt (fun z => ∏ n ∈ s, f n z) x = ∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.support_inv' : ∀ {ι : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] (f : ι → G₀), Function.support f⁻¹ = Function.support f
-- Std.Http.Protocol.H1
/-- Marks outgoing bodies as omitted when response semantics (or HEAD method) require
header-only responses.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.maybeSuppressOutgoingBody : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Message.Head dir.swap → Std.Http.Protocol.H1.Machine dir
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.toGraphviz.go.match_1.eq_3 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (lhs rhs : Std.Sat.AIG.Fanin)
  (h_1 : Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx : α) → Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx))
  (h_3 :
    (lhs_1 rhs_1 : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.gate lhs_1 rhs_1 → motive (Std.Sat.AIG.Decl.gate lhs_1 rhs_1)),
  (match elem : Std.Sat.AIG.Decl.gate lhs rhs with
    | Std.Sat.AIG.Decl.false => h_1 elem
    | Std.Sat.AIG.Decl.atom idx => h_2 idx elem
    | Std.Sat.AIG.Decl.gate lhs_1 rhs_1 => h_3 lhs_1 rhs_1 elem) =
    h_3 lhs rhs ⋯
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
CategoryTheory.Over.conePostIso_hom_app_hom : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) (i : J) (X : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Over.conePostIso F i).hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.Algebra.Homology.BifunctorFlip
/-- The canonical isomorphism `mapBifunctor K₂ K₁ F.flip c ≅ mapBifunctor K₁ K₂ F c`.  -/
HomologicalComplex.mapBifunctorFlipIso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            {I₁ : Type u_4} →
              {I₂ : Type u_5} →
                {J : Type u_6} →
                  {c₁ : ComplexShape I₁} →
                    {c₂ : ComplexShape I₂} →
                      [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                        [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                          [inst_5 : CategoryTheory.Preadditive D] →
                            (K₁ : HomologicalComplex C₁ c₁) →
                              (K₂ : HomologicalComplex C₂ c₂) →
                                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                  [inst_6 : F.PreservesZeroMorphisms] →
                                    [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                      (c : ComplexShape J) →
                                        [inst_8 : TotalComplexShape c₁ c₂ c] →
                                          [inst_9 : TotalComplexShape c₂ c₁ c] →
                                            [inst_10 : TotalComplexShapeSymmetry c₁ c₂ c] →
                                              [inst_11 : DecidableEq J] →
                                                [inst_12 : K₁.HasMapBifunctor K₂ F c] →
                                                  K₂.mapBifunctor K₁ F.flip c ≅ K₁.mapBifunctor K₂ F c
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instReprOverlaps : Repr Lean.Meta.Match.Overlaps
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.transpose_iff : ∀ {n : Type u_2} {R' : Type u_4} [inst : CommRing R'] [inst_1 : PartialOrder R'] [inst_2 : StarRing R']
  {M : Matrix n n R'}, M.transpose.PosDef ↔ M.PosDef
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.eval : Std.Tactic.BVDecide.Gate → Bool → Bool → Bool
-- Mathlib.RingTheory.Trace.Basic
Algebra.traceMatrix.eq_1 : ∀ {κ : Type w} (A : Type u) {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (b : κ → B),
  Algebra.traceMatrix A b = Matrix.of fun i j => ((Algebra.traceForm A B) (b i)) (b j)
-- Mathlib.Algebra.Quaternion
Quaternion.re_natCast : ∀ {R : Type u_3} [inst : CommRing R] (n : ℕ), (↑n).re = ↑n
-- Mathlib.Algebra.Order.Interval.Basic
Interval.bot_sub : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst_4 : AddLeftMono α] (t : Interval α), ⊥ - t = ⊥
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
LinearIsometry.Simps.apply : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring R₂] →
        (σ₁₂ : R →+* R₂) →
          (E : Type u_11) →
            (E₂ : Type u_12) →
              [inst_2 : SeminormedAddCommGroup E] →
                [inst_3 : SeminormedAddCommGroup E₂] →
                  [inst_4 : Module R E] → [inst_5 : Module R₂ E₂] → (E →ₛₗᵢ[σ₁₂] E₂) → E → E₂
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjointAux_unique : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  [inst_5 : CompleteSpace E] (hT : Dense ↑T.domain) (y : ↥T.adjointDomain) {x₀ : E},
  (∀ (x : ↥T.domain), inner 𝕜 x₀ ↑x = inner 𝕜 (↑y) (↑T x)) → (LinearPMap.adjointAux hT) y = x₀
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.Std.Do.PredTrans.pushOption.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Topology.Sheaves.Flasque
CategoryTheory.instCategoryStructuredArrow.hcongr_6 : ∀ (C C' : Type u₁),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v₁, u₁} C) (inst' : CategoryTheory.Category.{v₁, u₁} C'),
      inst ≍ inst' →
        ∀ (D D' : Type u₂),
          D = D' →
            ∀ (inst_1 : CategoryTheory.Category.{v₂, u₂} D) (inst'_1 : CategoryTheory.Category.{v₂, u₂} D'),
              inst_1 ≍ inst'_1 →
                ∀ (S : D) (S' : D'),
                  S ≍ S' →
                    ∀ (T : CategoryTheory.Functor C D) (T' : CategoryTheory.Functor C' D'),
                      T ≍ T' → CategoryTheory.instCategoryStructuredArrow ≍ CategoryTheory.instCategoryStructuredArrow
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Context.mk.sizeOf_spec : ∀ (useMT : Bool) (thm : Lean.Meta.Grind.EMatchTheorem) (initApp : Lean.Expr),
  sizeOf { useMT := useMT, thm := thm, initApp := initApp } = 1 + sizeOf useMT + sizeOf thm + sizeOf initApp
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netMaxcard_antitone : ∀ {X : Type u_1} (T : X → X) (F : Set X) (n : ℕ), Antitone fun U => Dynamics.netMaxcard T F U n
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.mk : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : outParam AlgebraicGeometry.AffineTargetMorphismProperty},
  Q.IsLocal → P = AlgebraicGeometry.targetAffineLocally Q → AlgebraicGeometry.HasAffineProperty P Q
-- Lean.Meta.Basic
/-- A simpler version of `ParamInfo` for information about the parameter of a forall or lambda.
 -/
Lean.Meta.ExprParamInfo : Type
-- Mathlib.Analysis.Normed.Group.Basic
enorm_sum_le_of_le : ∀ {ι : Type u_3} {ε : Type u_8} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddCommMonoid ε] (s : Finset ι)
  {f : ι → ε} {n : ι → ENNReal}, (∀ b ∈ s, ‖f b‖ₑ ≤ n b) → ‖∑ b ∈ s, f b‖ₑ ≤ ∑ b ∈ s, n b
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instSecondCountableTopology : ∀ {M : Type u_1} [inst : TopologicalSpace M] [SecondCountableTopology M], SecondCountableTopology Mᵈᵃᵃ
-- Init.Data.Dyadic.Basic
Dyadic.roundDown.eq_1 : ∀ (prec : ℤ), Dyadic.zero.roundDown prec = Dyadic.zero
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.pairwiseDisjoint_piAntidiag_map_addRightEmbedding : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCancelCommMonoid μ]
  [inst_2 : Finset.HasAntidiagonal μ] [inst_3 : DecidableEq μ] {i : ι} {s : Finset ι},
  i ∉ s →
    ∀ (n : μ),
      (↑(Finset.HasAntidiagonal.antidiagonal n)).PairwiseDisjoint fun p =>
        Finset.map (addRightEmbedding fun j => if j = i then p.1 else 0) (s.piAntidiag p.2)
-- Mathlib.GroupTheory.GroupAction.Hom
VAddCommClass.toAddActionHom.eq_1 : ∀ {M : Type u_11} (N : Type u_9) (α : Type u_10) [inst : VAdd M α] [inst_1 : VAdd N α] [inst_2 : VAddCommClass M N α]
  (c : M), VAddCommClass.toAddActionHom N α c = { toFun := fun x => c +ᵥ x, map_vadd' := ⋯ }
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.norm.eq_2 : ∀ (k : ℤ) (v : Int.Internal.Linear.Var) (p_2 : Int.Internal.Linear.Poly),
  (Int.Internal.Linear.Poly.add k v p_2).norm = Int.Internal.Linear.Poly.insert k v p_2.norm
-- Mathlib.Data.Nat.Totient
Nat.totient_mul : ∀ {m n : ℕ}, m.Coprime n → (m * n).totient = m.totient * n.totient
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_sum_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  [MeasureTheory.IsFiniteMeasure μ] [inst : Fintype ι],
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.covariance (fun ω => ∑ i, X i ω) Y μ = ∑ i, ProbabilityTheory.covariance (X i) Y μ
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that
`f(S) ⊆ AddUnits N`, for all `x₁ x₂ : M` and `y₁, y₂ ∈ S`, we have
`f x₁ - f y₁ = f x₂ - f y₂ ↔ f (x₁ + y₂) = f (x₂ + y₁)`.  -/
AddSubmonoid.LocalizationMap.add_neg : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {f : M →+ N}
  (h : ∀ (y : ↥S), IsAddUnit (f ↑y)) {x₁ x₂ : M} {y₁ y₂ : ↥S},
  f x₁ + ↑(-(IsAddUnit.liftRight (f.domRestrict S) h) y₁) = f x₂ + ↑(-(IsAddUnit.liftRight (f.domRestrict S) h) y₂) ↔
    f (x₁ + ↑y₂) = f (x₂ + ↑y₁)
-- Mathlib.Algebra.BigOperators.Finprod
AddEquiv.map_finsum : ∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (g : M ≃+ N)
  (f : α → M), g (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g (f i)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.eq_inv_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z},
  g = CategoryTheory.CategoryStruct.comp α.inv f ↔ CategoryTheory.CategoryStruct.comp α.hom g = f
-- Std.Async.System
Std.Async.System.instInhabitedEnvironment.default : Std.Async.System.Environment
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.whiskeringRight_preservesColimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasColimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfShape J F],
  CategoryTheory.Limits.PreservesColimitsOfShape J ((CategoryTheory.Functor.whiskeringRight C D E).obj F)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_add_apply_of_not_exists_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Add M] (r : R) {g g' : M} (x : AddMonoidAlgebra R M),
  (¬∃ d, g' = g + d) → (AddMonoidAlgebra.single g r * x).coeff g' = 0
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressEnd.mk.injEq : ∀ (kind : String) (message? : Option String) (kind_1 : String) (message?_1 : Option String),
  ({ kind := kind, message? := message? } = { kind := kind_1, message? := message?_1 }) =
    (kind = kind_1 ∧ message? = message?_1)
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.symm_apply_mem_iff_mem_image : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (x : β), e.symm x ∈ s ↔ x ∈ ⇑e '' s
-- Mathlib.Logic.Basic
iff_iff_and_or_not_and_not : ∀ {a b : Prop}, (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b
-- Std.Http.Data.Body.Length
Std.Http.Body.Length.fixed.injEq : ∀ (n n_1 : ℕ), (Std.Http.Body.Length.fixed n = Std.Http.Body.Length.fixed n_1) = (n = n_1)
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatTrans.naturality_2_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) {Z : D} (h : G.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map e.hom)
      (CategoryTheory.CategoryStruct.comp (α.app Y) (CategoryTheory.CategoryStruct.comp (G.map e.inv) h)) =
    CategoryTheory.CategoryStruct.comp (α.app X) h
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.map_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {α₁ : Type u_6} {g : α₁ → α} {x : FreeAddMonoid α₁},
  (FreeAddMonoid.map f) ((FreeAddMonoid.map g) x) = (FreeAddMonoid.map (f ∘ g)) x
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galLiftEquiv.eq_1 : ∀ {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [inst : CommRing A]
  [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : Field K]
  [inst_6 : Field L] [inst_7 : Field L₂] [inst_8 : Algebra A K] [inst_9 : IsFractionRing A K] [inst_10 : Algebra K L]
  [inst_11 : Algebra A L] [inst_12 : IsScalarTower A K L] [inst_13 : Algebra K L₂] [inst_14 : Algebra A L₂]
  [inst_15 : IsScalarTower A K L₂] [inst_16 : Algebra B L] [inst_17 : IsScalarTower A B L]
  [inst_18 : IsIntegralClosure B A L] [inst_19 : Algebra B₂ L₂] [inst_20 : IsScalarTower A B₂ L₂]
  [inst_21 : IsIntegralClosure B₂ A L₂] [inst_22 : Algebra.IsAlgebraic K L] [inst_23 : Algebra.IsAlgebraic K L₂]
  (σ : B ≃ₐ[A] B₂), galLiftEquiv K L L₂ σ = AlgEquiv.ofAlgHom (galLift K L L₂ ↑σ) (galLift K L₂ L ↑σ.symm) ⋯ ⋯
-- Mathlib.Analysis.Normed.Affine.AddTorsorBases
/-- The affine span of a nonempty open set is `⊤`.  -/
IsOpen.affineSpan_eq_top : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {u : Set P}, IsOpen u → u.Nonempty → affineSpan ℝ u = ⊤
-- Std.Data.TreeSet.Basic
/-- Folds the given function over the elements of the tree set in descending order.  -/
Std.TreeSet.foldr : {α : Type u} → {cmp : α → α → Ordering} → {δ : Type w} → (α → δ → δ) → δ → Std.TreeSet α cmp → δ
-- Mathlib.NumberTheory.ZetaValues
bernoulliFun_zero : ∀ (x : ℝ), bernoulliFun 0 x = 1
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.preconnected_of_ediam_ne_top : ∀ {α : Type u_1} {G : SimpleGraph α}, G.ediam ≠ ⊤ → G.Preconnected
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.natAddLEFunctor_obj' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n k l i : ℕ} (h : k + l ≤ n)
  (R : CategoryTheory.ComposableArrows C n)
  (x : autoParam (i ≤ l) CategoryTheory.ComposableArrows.natAddLEFunctor_obj'._auto_1),
  ((CategoryTheory.ComposableArrows.natAddLEFunctor h).obj R).obj' i x = R.obj' (k + i) ⋯
-- Init.Prelude
/-- Gets the position information from a `SourceInfo`, if available.
If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
will also return `none`.
 -/
Lean.SourceInfo.getPos? : Lean.SourceInfo → optParam Bool false → Option String.Pos.Raw
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `UniformCauchySeqOn.add` -/
UniformCauchySeqOn.fun_add : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {s : Set β},
  UniformCauchySeqOn f l s → UniformCauchySeqOn f' l s → UniformCauchySeqOn (fun i i_1 => f i i_1 + f' i i_1) l s
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.C 1 = 1
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.add_overlap_pf_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {a b : R} (x : R) (e : ℕ),
  Mathlib.Meta.NormNum.IsNat (a + b) 0 → Mathlib.Meta.NormNum.IsNat (x ^ e * a + x ^ e * b) 0
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.vecMul_swap : ∀ {R : Type u_1} {n : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j : n) (a : n → R),
  Matrix.vecMul a (Matrix.swap R i j) = a ∘ ⇑(Equiv.swap i j)
-- Mathlib.Combinatorics.Enumerative.Bell
_private.Mathlib.Combinatorics.Enumerative.Bell.0.Nat.bell.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Init.Data.BitVec.Basic
BitVec.ushiftRight_eq : ∀ {w : ℕ} (x : BitVec w) (n : ℕ), x.ushiftRight n = x >>> n
-- Init.MetaTypes
/-- If `locals` is `true`, `simp` will unfold all definitions from the current file.
For local theorems, use `+suggestions` instead.
 -/
Lean.Meta.Simp.Config.locals : Lean.Meta.Simp.Config → Bool
-- Init.Data.Vector.Lemmas
Vector.flatten_mk : ∀ {α : Type u_1} {n m : ℕ} {xss : Array (Vector α n)} (h : xss.size = m),
  (Vector.mk xss h).flatten = Vector.mk (Array.map Vector.toArray xss).flatten ⋯
-- Init.Data.List.ToArray
List.forIn'_loop_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (l : List α)
  (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : ℕ) (h : i ≤ l.length) (b : β),
  Array.forIn'.loop l.toArray f i h b = forIn' (List.drop (l.length - i) l) b fun a m b => f a ⋯ b
-- Lean.Parser.Command
Lean.Parser.Command.where.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.positional : Lean.Name → Lean.Expr → Lean.Doc.ArgSpec✝
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.elemExponent_eq_zero_of_charZero : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] (a : L) [CharZero K], IsPurelyInseparable.elemExponent K a = 0
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_zpow_of_nonpos₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 0 < a → a ≤ 1 → n ≤ 0 → 1 ≤ a ^ n
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_nsmul_eq_zero : ∀ {G : Type u} [inst : AddMonoid G] (g : G), AddMonoid.exponent G • g = 0
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild.match_1.eq_4 : ∀ (motive : Lean.Expr → Sort u_1) (fvarId : Lean.FVarId) (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a))
  (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (e : Lean.Expr) → motive e),
  (match Lean.Expr.fvar fvarId with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | e => h_7 e) =
    h_4 fvarId
-- Init.Data.SInt.Lemmas
Int16.mul_zero : ∀ {a : Int16}, a * 0 = 0
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorAlgebra.mk_reindex_cast : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n m : ℕ}
  (h : n = m) (x : TensorPower R n M),
  GradedMonoid.mk m ((PiTensorProduct.reindex R (fun x => M) (Equiv.cast ⋯)) x) = GradedMonoid.mk n x