mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.ofMapMulInv.eq_1 : ∀ {G : Type u_5} [inst : Group G] {H : Type u_8} [inst_1 : Group H] (f : G → H)
  (map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹), MonoidHom.ofMapMulInv f map_div = MonoidHom.mk' f ⋯
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_add_erase : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (x : AddMonoidAlgebra R M),
  AddMonoidAlgebra.single m (x.coeff m) + AddMonoidAlgebra.erase m x = x
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_add : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x y : WittVector p R),
  WittVector.ghostFun✝ (x + y) = WittVector.ghostFun✝ x + WittVector.ghostFun✝ y
-- Init.Data.SInt.Lemmas
Int8.toUInt8_ofNat' : ∀ {n : ℕ}, (Int8.ofNat n).toUInt8 = UInt8.ofNat n
-- Mathlib.GroupTheory.GroupAction.OfQuotient
MulAction.instQuotientSubgroupElemFixedPointsSubtypeMem : {G : Type u_1} →
  [inst : Group G] →
    {A : Type u_2} →
      [inst_1 : MulAction G A] →
        {H : Subgroup G} → [inst_2 : H.Normal] → MulAction (G ⧸ H) ↑(MulAction.fixedPoints (↥H) A)
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.isGE_Q_obj_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (K : CochainComplex C ℤ) (n : ℤ), (DerivedCategory.Q.obj K).IsGE n ↔ K.IsGE n
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.nnnorm_eq : ∀ {𝕜 : Type u_7} [inst : RCLike 𝕜] {n : Type u_8} [inst_1 : Fintype n] (x : EuclideanSpace 𝕜 n),
  ‖x‖₊ = NNReal.sqrt (∑ i, ‖x.ofLp i‖₊ ^ 2)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_natCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIcoMod hp (a + ↑m * p) b = toIcoMod hp a b + ↑m * p
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.LocalizationMap.nonZeroDivisors_le_comap : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  (f : S.LocalizationMap N), nonZeroDivisors M ≤ Submonoid.comap f (nonZeroDivisors N)
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
/-- The composition of the normalizing isomorphisms `η_f : p ⊗ f ≅ pf` and `η_g : pf ⊗ g ≅ pfg`.  -/
Mathlib.Tactic.Monoidal.normalizeIsoComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {p f g pf pfg : C} →
        (CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf) →
          (CategoryTheory.MonoidalCategoryStruct.tensorObj pf g ≅ pfg) →
            (CategoryTheory.MonoidalCategoryStruct.tensorObj p (CategoryTheory.MonoidalCategoryStruct.tensorObj f g) ≅
              pfg)
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_map : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure Ω'} {Y : Ω' → Ω},
  AEMeasurable X (MeasureTheory.Measure.map Y μ) →
    AEMeasurable Y μ →
      ProbabilityTheory.variance X (MeasureTheory.Measure.map Y μ) = ProbabilityTheory.variance (X ∘ Y) μ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.below.cons : ∀
  {motive :
    {basis : Tactic.ComputeAsymptotics.Basis} →
      (a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis) → a.Trimmed → Prop}
  {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl} {f : ℝ → ℝ}
  (h_trimmed : coef.Trimmed) (h_ne_zero : ¬coef.IsZero),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.below h_trimmed →
    motive coef h_trimmed → Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.below ⋯
-- Mathlib.Order.Bounds.Basic
IsCofinalFor.rfl : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsCofinalFor s s
-- Mathlib.Algebra.Lie.Weights.RootSystem
/-- Members of the `α`-chain through `β` are the only roots of the form `β - kα`.  -/
LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  α.IsNonZero →
    ∀ (n : ℤ),
      LieAlgebra.rootSpace H (n • ⇑α + ⇑β) ≠ ⊥ ↔
        n ≤ ↑(LieModule.chainTopCoeff (⇑α) β) ∧ -n ≤ ↑(LieModule.chainBotCoeff (⇑α) β)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.Even.eval_neg : ∀ {S : Type u_2} [inst : CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) (x : ZMod m), ψ.Even → ψ (-x) = ψ x
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsSymm.sub : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B₁ B₂ : LinearMap.BilinForm R₁ M₁}, B₁.IsSymm → B₂.IsSymm → (B₁ - B₂).IsSymm
-- Mathlib.Topology.Algebra.Group.Basic
inv_mem_nhds_one : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {S : Set G},
  S ∈ nhds 1 → S⁻¹ ∈ nhds 1
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- **Alias** of `Metric.eventually_nhds_zero_forall_closedEBall_subset`.

---

Let `K : ι → Set X` be a locally finite family of closed sets in an emetric space. Let
`U : ι → Set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then for any point
`x : X`, for sufficiently small `r : ℝ≥0∞` and for `y` sufficiently close to `x`, for all `i`, if
`y ∈ K i`, then `Metric.closedEBall y r ⊆ U i`.  -/
EMetric.eventually_nhds_zero_forall_closedBall_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K →
          ∀ (x : X), ∀ᶠ (p : ENNReal × X) in nhds 0 ×ˢ nhds x, ∀ (i : ι), p.2 ∈ K i → Metric.closedEBall p.2 p.1 ⊆ U i
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotationAux₁.congr_simp : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o o_1 : Orientation ℝ E (Fin 2)), o = o_1 → o.rightAngleRotationAux₁ = o_1.rightAngleRotationAux₁
-- Lean.Data.Lsp.Internal
Lean.Lsp.instBEqRefIdent : BEq Lean.Lsp.RefIdent
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.preimage : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X} {H : Type u_3} {Y : Type u_4}
  [inst_2 : AddGroup H] [inst_3 : AddAction H Y] {φ : H → G} (j : Y →ₑ[φ] X),
  AddAction.IsBlock G B → AddAction.IsBlock H (⇑j ⁻¹' B)
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
_private.Mathlib.AlgebraicTopology.DoldKan.Normalized.0.AlgebraicTopology.NormalizedMooreComplex.objX.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryGE : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        (k : α) →
          (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.Ordered → (∃ a ∈ t, (compare a k).isGE = true) → α × β
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.liftOfStrictSegal.naturalityProperty_eq_top : ∀ {X Y : SSet.Truncated 2}
  (f₀ :
    X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))
  (f₁ :
    X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }))
  (hδ₁ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hδ₀ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) (f₁ x)),
  (∀ (x : X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ }))
      (y : Y.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })),
      f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op)) x) =
          (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op)) y →
        f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op)) x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op)) y →
          f₁
              ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝ _proof_15✝).op))
                x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝ _proof_15✝).op)) y) →
    (∀ (x : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })),
        f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝ _proof_11✝).op)) x) =
          (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝ _proof_11✝).op))
            (f₀ x)) →
      ∀ (hY : Y.StrictSegal), SSet.Truncated.liftOfStrictSegal.naturalityProperty f₀ f₁ hδ₁ hδ₀ hY = ⊤
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.range_pullback_to_prod : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z),
  Set.range
      ⇑(CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g)
            (CategoryTheory.Limits.pullback.snd f g))) =
    {x |
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g)) x}
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableAt.rpow_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {p : ℝ},
  DifferentiableAt ℝ f x → f x ≠ 0 ∨ 1 ≤ p → DifferentiableAt ℝ (fun x => f x ^ p) x
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
EReal.exp_nmul : ∀ (x : EReal) (n : ℕ), (↑n * x).exp = x.exp ^ n
-- Mathlib.Probability.Moments.MGFAnalytic
/-- The derivatives of the moment-generating function at zero are the moments.  -/
ProbabilityTheory.iteratedDeriv_mgf_zero : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  0 ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ), iteratedDeriv n (ProbabilityTheory.mgf X μ) 0 = ∫ (x : Ω), (X ^ n) x ∂μ
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
IsBoundedBilinearMap.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {b : E × F → G} {u : Set (E × F)},
  IsBoundedBilinearMap 𝕜 b → DifferentiableOn 𝕜 b u
-- Init.Data.UInt.Basic
/-- Bitwise and for 16-bit unsigned integers. Usually accessed via the `&&&` operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.land : UInt16 → UInt16 → UInt16
-- Std.Data.DTreeMap.Lemmas
/-- Variant of `get!_map` that holds without `LawfulEqCmp`.  -/
Std.DTreeMap.Const.get!_map' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited γ] {f : α → β → γ} {k : α},
  Std.DTreeMap.Const.get! (Std.DTreeMap.map f t) k =
    (Option.pmap (fun v h => f (t.getKey k h) v) (Std.DTreeMap.Const.get? t k) ⋯).get!
-- Lean.Meta.Tactic.Symm
/-- Use a symmetry lemma (i.e. marked with `@[symm]`) to replace a hypothesis in a goal.  -/
Lean.MVarId.applySymmAt : Lean.FVarId → Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.denom_dvd : ∀ {K : Type u} [inst : Field K] {x : RatFunc K} {q : Polynomial K},
  q ≠ 0 → (x.denom ∣ q ↔ ∃ p, x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Submodule.mem_toSubalgebra : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {p : Submodule R A}
  {h_one : 1 ∈ p} {h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p} {x : A}, x ∈ p.toSubalgebra h_one h_mul ↔ x ∈ p
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.IsModHom.smul_hom : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {A : C} {inst_4 : CategoryTheory.MonObj A} {M N : D} {inst_5 : CategoryTheory.ModObj A M}
  {inst_6 : CategoryTheory.ModObj A N} {f : M ⟶ N} [self : CategoryTheory.IsModHom A f],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
      CategoryTheory.ModObj.smul
-- Mathlib.ModelTheory.Order
FirstOrder.Language.order.instStrongHomClassOrderEmbedding : ∀ {M : Type w'} [inst : FirstOrder.Language.order.Structure M] [inst_1 : LE M]
  [FirstOrder.Language.order.OrderedStructure M] {N : Type u_1} [inst_3 : FirstOrder.Language.order.Structure N]
  [inst_4 : LE N] [FirstOrder.Language.order.OrderedStructure N], FirstOrder.Language.order.StrongHomClass (M ↪o N) M N
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v v' : α} [Std.TransCmp cmp] {t : RBTree.RBSet α cmp},
  v' ∈ t.insert v ↔ v' ∈ t ∨ cmp v v' = Ordering.eq
-- Lean.LabelAttribute
/-- Helper function for `registerLabelAttr`.  -/
Lean.mkLabelAttr : Lean.Name → String → Lean.LabelExtension → autoParam Lean.Name Lean.mkLabelAttr._auto_1 → IO Unit
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `M` is a commutative additive monoid object, then `Hom(X, M)` has a commutative additive
monoid structure.  -/
CategoryTheory.Hom.addCommMonoid : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {M X : C} →
        [inst_2 : CategoryTheory.AddMonObj M] →
          [inst_3 : CategoryTheory.BraidedCategory C] → [CategoryTheory.IsCommAddMonObj M] → AddCommMonoid (X ⟶ M)
-- Init.Data.UInt.Bitwise
USize.toUInt32_or : ∀ (a b : USize), (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32
-- Init.Data.Nat.Lemmas
Nat.add_lt_add_of_lt_of_le : ∀ {a b c d : ℕ}, a < b → c ≤ d → a + c < b + d
-- Mathlib.Analysis.CStarAlgebra.Fuglede
/-- **Fuglede–Putnam–Rosenblum**: If `a` is a normal element in a C⋆-algebra `A` which
commutes with `x`, then `star a` commutes with `x`.  -/
IsStarNormal.commute_star_right : ∀ {A : Type u_2} [inst : NonUnitalCStarAlgebra A] {a x : A}, IsStarNormal a → Commute x a → Commute x (star a)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_of_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [IsEmpty α] (f : α → β),
  Measurable f
-- Batteries.Data.ByteArray
ByteArray.get_ofFn : ∀ {n : ℕ} (f : Fin n → UInt8) (i : Fin (ByteArray.ofFn f).size), (ByteArray.ofFn f).get ↑i ⋯ = f (Fin.cast ⋯ i)
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.subNegMonoid : {α : Type u} → [h : DivInvMonoid α] → SubNegMonoid (Additive α)
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.instResiduallyFiniteSubtypeMemAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] [AddGroup.ResiduallyFinite G] {H : AddSubgroup G}, AddGroup.ResiduallyFinite ↥H
-- Lean.Elab.Term.TermElabM
/-- Adapt a syntax transformation to a regular, term-producing elaborator.  -/
Lean.Elab.Term.adaptExpander : (Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax) → Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
CommMonTypeEquivalenceCommMon.commMonCommMonoid : (A : Type u) → [inst : CategoryTheory.MonObj A] → [CategoryTheory.IsCommMonObj A] → CommMonoid A
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- Eta-expanded form of `fderiv_id` -/
fderiv_fun_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [T2Space E],
  fderiv 𝕜 (fun x => x) x = ContinuousLinearMap.id 𝕜 E
-- Mathlib.Order.Interval.Finset.Basic
Finset.instUniqueSubtypeMemIicBot : {α : Type u_2} →
  [inst : PartialOrder α] → [inst_1 : LocallyFiniteOrder α] → [inst_2 : OrderBot α] → Unique ↥(Finset.Iic ⊥)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setAverage_eq : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (μ : MeasureTheory.Measure α) (f : α → E) (s : Set α), ⨍ (x : α) in s, f x ∂μ = (μ.real s)⁻¹ • ∫ (x : α) in s, f x ∂μ
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_iSup : ∀ {ι : Sort u_1} {a : ENNReal} [Nonempty ι] (f : ι → ENNReal), a + ⨆ i, f i = ⨆ i, a + f i
-- Init.Data.Range.Polymorphic.Map
Std.PRange.LawfulUpwardEnumerable.ofMap : ∀ {α : Type u_2} {β : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [Std.PRange.LawfulUpwardEnumerable β] (f : Std.PRange.UpwardEnumerable.Map α β), Std.PRange.LawfulUpwardEnumerable α
-- Mathlib.Order.Category.PartOrdEmb
/-- Isomorphisms in `PartOrdEmb` correspond to order isomorphisms.  -/
PartOrdEmb.orderIsoEquivIso : {α β : PartOrdEmb} → (α ≅ β) ≃ (↑α ≃o ↑β)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by swapping components.  -/
ContinuousMonoidHom.swap : (A : Type u_2) →
  (B : Type u_3) →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → A × B →ₜ* B × A
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inr_sub : ∀ (R : Type u_3) {A : Type u_4} [inst : AddGroup R] [inst_1 : AddGroup A] (m₁ m₂ : A), ↑(m₁ - m₂) = ↑m₁ - ↑m₂
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.prod_inf_prod : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B] [inst_7 : StarRing R]
  [inst_8 : IsScalarTower R A A] [inst_9 : SMulCommClass R A A] [inst_10 : StarModule R A]
  [inst_11 : IsScalarTower R B B] [inst_12 : SMulCommClass R B B] [inst_13 : StarModule R B]
  {S T : NonUnitalStarSubalgebra R A} {S₁ T₁ : NonUnitalStarSubalgebra R B},
  S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)
-- Lean.Elab.Do.Legacy
/-- Return true if we should not lift `(<- ...)` actions nested in the syntax nodes with the given kind.  -/
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.nestedActionDelimiter : Lean.SyntaxNodeKind → Bool
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.eq_1 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_1 ()
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C n}
  (app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i)
  (w :
    ∀ (i : ℕ) (hi : i < n),
      CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩).hom =
        CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩).hom (G.map' i (i + 1) ⋯ hi)),
  (CategoryTheory.ComposableArrows.isoMk app w).hom = CategoryTheory.ComposableArrows.homMk (fun i => (app i).hom) w
-- Mathlib.Topology.ContinuousMap.Defs
/-- See note [custom simps projection].  -/
ContinuousMap.Simps.apply : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → C(X, Y) → X → Y
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (P : CategoryTheory.ObjectProperty C)
  [inst_4 : P.IsSerreClass] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F]
  [CategoryTheory.Limits.PreservesFiniteColimits F], P.isoModSerre.IsInvertedBy F ↔ P ≤ F.kernel
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- A clique in a graph is a set of vertices that are pairwise adjacent.  -/
SimpleGraph.IsClique : {α : Type u_1} → SimpleGraph α → Set α → Prop
-- Mathlib.Order.Filter.CountablyGenerated
Filter.exists_antitone_seq : ∀ {α : Type u_1} (f : Filter α) [f.IsCountablyGenerated], ∃ x, Antitone x ∧ ∀ {s : Set α}, s ∈ f ↔ ∃ i, x i ⊆ s
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instHashableArg : {pu : Lean.Compiler.LCNF.Purity} → Hashable (Lean.Compiler.LCNF.Arg pu)
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_binop_subset : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : One M] [inst_1 : One N] [inst_2 : One P]
  (op : M → N → P),
  op 1 1 = 1 →
    ∀ (f : ι → M) (g : ι → N),
      (Function.mulSupport fun x => op (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g
-- Mathlib.Order.Lattice
/-- A subtype forms a `⊔`-semilattice if `⊔` preserves the property.
See note [reducible non-instances].  -/
Subtype.semilatticeSup : {α : Type u} →
  [inst : SemilatticeSup α] → {P : α → Prop} → (∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) → SemilatticeSup { x // P x }
-- Mathlib.GroupTheory.Rank
AddSubgroup.rank_closure_finite_le_nat_card : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G) [inst_1 : Finite ↑s],
  AddGroup.rank ↥(AddSubgroup.closure s) ≤ Nat.card ↑s
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.instHasInjectiveDimensionLTHAddNat_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n : ℕ)
  [CategoryTheory.HasInjectiveDimensionLT X n] (k : ℕ), CategoryTheory.HasInjectiveDimensionLT X (k + n)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- A non-unital `R`-algebra homomorphism from `R[M]` is uniquely defined by its
values on the monomials `single a 1`.  -/
MonoidAlgebra.nonUnitalAlgHom_ext : ∀ (R : Type u_1) {A : Type u_4} {M : Type u_7} [inst : Semiring R] [inst_1 : Mul M]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] {φ₁ φ₂ : MonoidAlgebra R M →ₙₐ[R] A},
  (∀ (x : M), φ₁ (MonoidAlgebra.single x 1) = φ₂ (MonoidAlgebra.single x 1)) → φ₁ = φ₂