mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.zero_lt_getElem!_toArray_rcc_iff : ∀ {m n i : ℕ}, 0 < (m...=n).toArray[i]! ↔ i < n + 1 - m ∧ 0 < i + m
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_eq_zero_iff`. -/
EMetric.diam_eq_zero_iff : ∀ {X : Type u_2} {s : Set X} [inst : EMetricSpace X], Metric.ediam s = 0 ↔ s.Subsingleton
-- Std.Sat.AIG.If
Std.Sat.AIG.instLawfulOperatorTernaryInputMkIfCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.TernaryInput Std.Sat.AIG.mkIfCached
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.normedAddCommGroup.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → NormedAddCommGroup (G i)],
  Pi.normedAddCommGroup =
    { toNorm := Pi.seminormedAddGroup.toNorm, toAddGroup := Pi.seminormedAddGroup.toAddGroup, add_comm := ⋯,
      toPseudoMetricSpace := Pi.seminormedAddGroup.toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.cancel_right : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : AddZero P]
  {g₁ g₂ : N →+ P} {f : M →+ N}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- A preadditive category has a weak equalizer for `f` and `g` if it has a weak
kernel for `f - g`.  -/
CategoryTheory.Preadditive.hasWeakEqualizer_of_hasWeakKernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (f g : X ⟶ Y) [CategoryTheory.Limits.HasWeakKernel (f - g)], CategoryTheory.Limits.HasWeakEqualizer f g
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.vComp_naturality_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.StrongTrans F G)
  (θ : CategoryTheory.Lax.StrongTrans G H) {a b : B} (f : a ⟶ b),
  ((η.vComp θ).naturality f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (θ.app b)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).inv (θ.app b))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (θ.app b)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f).inv)
            (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (H.map f)).inv)))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.contains_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (Std.ExtDTreeMap.Const.insertMany t l).contains k = (t.contains k || (List.map Prod.fst l).contains k)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_insertMany_emptyWithCapacity_list_le : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)}, (↑↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).size ≤ l.length
-- Init.Data.String.Iterate
/-- Creates an iterator over all characters \(Unicode code points\) in `s`, starting from the end
of the slice and iterating towards the start.

Example:

* `"abc".revChars.toList = ['c', 'b', 'a']`

* `"ab∀c".revChars.toList = ['c', '∀', 'b', 'a']`
 -/
String.revChars : (s : String) → Std.Iter Char
-- Mathlib.Algebra.Order.Module.Archimedean
ArchimedeanClass.congr_simp : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  ArchimedeanClass M = ArchimedeanClass M
-- Mathlib.ModelTheory.Order
/-- Any linearly-ordered type is naturally a structure in the language `Language.order`.
This is not an instance, because sometimes the `Language.order.Structure` is defined first.  -/
FirstOrder.Language.orderStructure : (M : Type w') → [LE M] → FirstOrder.Language.order.Structure M
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.limitAddCommGroup.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections],
  AddCommGrpCat.limitAddCommGroup F =
    {
      add :=
        AddCommGrpCat.limitAddCommGroup._aux_1 F
          (AddGrpCat.sectionsAddSubgroup (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat))).toAddCommGroup,
      add_assoc := ⋯,
      zero :=
        AddCommGrpCat.limitAddCommGroup._aux_4 F
          (AddGrpCat.sectionsAddSubgroup (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat))).toAddCommGroup,
      zero_add := ⋯, add_zero := ⋯,
      nsmul :=
        AddCommGrpCat.limitAddCommGroup._aux_8 F
          (AddGrpCat.sectionsAddSubgroup (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat))).toAddCommGroup,
      nsmul_zero := ⋯, nsmul_succ := ⋯,
      neg :=
        AddCommGrpCat.limitAddCommGroup._aux_12 F
          (AddGrpCat.sectionsAddSubgroup (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat))).toAddCommGroup,
      sub :=
        AddCommGrpCat.limitAddCommGroup._aux_14 F
          (AddGrpCat.sectionsAddSubgroup (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat))).toAddCommGroup,
      zsmul :=
        AddCommGrpCat.limitAddCommGroup._aux_16 F
          (AddGrpCat.sectionsAddSubgroup (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat))).toAddCommGroup,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯, add_comm := ⋯ }
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.smulMemClass : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A], SMulMemClass (StarSubalgebra R A) R A
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.mk'.hcongr_3 : ∀ (X X' : SSet),
  X = X' →
    ∀ (toS : X.S) (toS' : X'.S),
      toS ≍ toS' →
        ∀ (nonDegenerate : toS.simplex ∈ X.nonDegenerate toS.dim)
          (nonDegenerate' : toS'.simplex ∈ X'.nonDegenerate toS'.dim),
          nonDegenerate ≍ nonDegenerate' →
            { toS := toS, nonDegenerate := nonDegenerate } ≍ { toS := toS', nonDegenerate := nonDegenerate' }
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.mul_const : ∀ {α : Type u_1} {f : α → α} {x : α} {m : ℕ}, Function.IsPeriodicPt f m x → ∀ (n : ℕ), Function.IsPeriodicPt f (m * n) x
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_eq_mul_mk'_one : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M),
  IsLocalization.mk' S x y = (algebraMap R S) x * IsLocalization.mk' S 1 y
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sin_pow_antitone : Antitone fun n => ∫ (x : ℝ) in 0..Real.pi, Real.sin x ^ n
-- Mathlib.CategoryTheory.Triangulated.Adjunction
CategoryTheory.Adjunction.IsTriangulated.leftAdjoint_isTriangulated : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.Limits.HasZeroObject C}
  {inst_3 : CategoryTheory.Limits.HasZeroObject D} {inst_4 : CategoryTheory.Preadditive C}
  {inst_5 : CategoryTheory.Preadditive D} {inst_6 : CategoryTheory.HasShift C ℤ} {inst_7 : CategoryTheory.HasShift D ℤ}
  {inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive}
  {inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive} {inst_10 : CategoryTheory.Pretriangulated C}
  {inst_11 : CategoryTheory.Pretriangulated D} {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {inst_12 : F.CommShift ℤ} {inst_13 : G.CommShift ℤ} [self : adj.IsTriangulated], F.IsTriangulated
-- Mathlib.Data.Seq.Basic
Stream'.Seq.map_tail : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream'.Seq α), Stream'.Seq.map f s.tail = (Stream'.Seq.map f s).tail
-- Mathlib.Data.Finsupp.ToDFinsupp
/-- The additive version of `Finsupp.toFinsupp`. Note that this is `noncomputable` because
`Finsupp.add` is noncomputable.  -/
finsuppLequivDFinsupp : {ι : Type u_1} →
  (R : Type u_2) →
    {M : Type u_3} →
      [DecidableEq ι] →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [(m : M) → Decidable (m ≠ 0)] → [inst_3 : Module R M] → (ι →₀ M) ≃ₗ[R] Π₀ (x : ι), M
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.nthRoot_one_left : Nat.nthRoot 1 = id
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_eq_toNNReal_iff : ∀ {r p : ℝ}, 0 ≤ r → 0 ≤ p → (r.toNNReal = p.toNNReal ↔ r = p)
-- Mathlib.Data.EReal.Operations
ENNReal.toEReal_sub : ∀ {x y : ENNReal}, y ≠ ⊤ → y ≤ x → ↑(x - y) = ↑x - ↑y
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.submoduleMap_coe_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {p : Submodule R M} (x : ↥p), ↑((f.submoduleMap p) x) = f ↑x
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_sub : ∀ {𝕜 : 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] {f g : E → F}
  {x : E} {s : Set E},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 f s x →
      DifferentiableWithinAt 𝕜 g s x → fderivWithin 𝕜 (f - g) s x = fderivWithin 𝕜 f s x - fderivWithin 𝕜 g s x
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instCompatibleValuation : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  (WithVal.valuation v).Compatible
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHintOptions.toJson : Lean.Lsp.InlayHintOptions → Lean.Json
-- Aesop.Forward.State
/-- The rule to which this state belongs.  -/
Aesop.RuleState.rule : Aesop.RuleState → Aesop.ForwardRule
-- Mathlib.Order.RelClasses
Std.Total.swap : ∀ {α : Type u} (r : α → α → Prop) [Std.Total r], Std.Total (Function.swap r)
-- Init.Data.Array.Lex.Lemmas
Array.le_iff_lt_or_eq : ∀ {α : Type u_1} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  [Std.Asymm fun x1 x2 => x1 < x2] {xs ys : Array α}, xs ≤ ys ↔ xs < ys ∨ xs = ys
-- Lean.Meta.Sym.SymM
/-- Information about a single argument position in a function's type signature.

This is used during pattern matching and structural definitional equality tests
to identify arguments that can be skipped or handled specially
(e.g., instance arguments can be synthesized, proof arguments can be inferred).
 -/
Lean.Meta.Sym.ProofInstArgInfo : Type
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.mk : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] {a : σ → MvPowerSeries τ S},
  (∀ (s : σ), IsNilpotent (MvPowerSeries.constantCoeff (a s))) →
    (∀ (d : τ →₀ ℕ), {s | (MvPowerSeries.coeff d) (a s) ≠ 0}.Finite) → MvPowerSeries.HasSubst a
-- Mathlib.Data.Nat.Cast.Commute
Commute.self_natCast_mul : ∀ {α : Type u_1} [inst : Semiring α] (a : α) (n : ℕ), Commute a (↑n * a)
-- Mathlib.Algebra.Category.Grp.Basic
AddEquiv.toAddCommGrpIso.eq_1 : ∀ {X Y : AddCommGrpCat} (e : ↑X ≃+ ↑Y),
  e.toAddCommGrpIso =
    { hom := AddCommGrpCat.ofHom e.toAddMonoidHom, inv := AddCommGrpCat.ofHom e.symm.toAddMonoidHom, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.Data.Multiset.FinsetOps
Multiset.subset_ndunion_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s ⊆ s.ndunion t
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.liftLeftHomology.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0)
  [inst_2 : S.HasLeftHomology],
  S.liftLeftHomology k hk = CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) S.leftHomologyπ
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precompose_map_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : G ⟶ F) {Y X : CategoryTheory.Limits.Cocone F} (f : Y ⟶ X),
  ((CategoryTheory.Limits.Cocone.precompose α).map f).hom = f.hom
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.valid : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α}, Ordnode.Valid' o₁ t o₂ → t.Valid
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.isClosed : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] (C : ProperCone R E), IsClosed ↑C
-- Mathlib.CategoryTheory.CommSq
/-- The square commutes.  -/
CategoryTheory.CommSq.w_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z},
  CategoryTheory.CommSq f g h i →
    ∀ {Z_1 : C} (h_1 : Z ⟶ Z_1),
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp h h_1) =
        CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp i h_1)
-- Init.Data.SInt.Basic
/-- The largest number that `Int64` can represent: `2^63 - 1 = 9223372036854775807`.  -/
Int64.maxValue : Int64
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_maxKey!_eq_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {hc : t.maxKey! ∈ t}, t.getKey t.maxKey! hc = t.maxKey ⋯
-- Mathlib.CategoryTheory.ComposableArrows.Three
CategoryTheory.ComposableArrows.threeδ₂Toδ₁_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {i j k l : C} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l)
  (f₁₂ : i ⟶ k) (f₂₃ : j ⟶ l) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃),
  (CategoryTheory.ComposableArrows.threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 1 = f₂
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isSome_getKey?_iff_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, (m.getKey? a).isSome = true ↔ a ∈ m
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.cyclesOpIso_inv_naturality_assoc : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] {Z : Vᵒᵖ} (h : K.op.cycles i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i).op
      (CategoryTheory.CategoryStruct.comp (K.cyclesOpIso i).inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (L.cyclesOpIso i).inv
        (HomologicalComplex.cyclesMap ((HomologicalComplex.opFunctor V c).map φ.op) i))
      h
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.ext_of_isSeparatedFor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type u_2)} {S : C}
  (E : CategoryTheory.PreZeroHypercover S),
  CategoryTheory.Presieve.IsSeparatedFor P E.presieve₀ →
    ∀ {x y : P.obj (Opposite.op S)},
      (∀ (i : E.I₀),
          (CategoryTheory.ConcreteCategory.hom (P.map (E.f i).op)) x =
            (CategoryTheory.ConcreteCategory.hom (P.map (E.f i).op)) y) →
        x = y
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_eq_get!_getElem? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {a : α}, m[a]! = m[a]?.get!
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr.0.Lean.Grind.CommRing.Mon.denoteExpr.go : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] →
          [Lean.Meta.Grind.Arith.CommRing.MonadRing M] → Lean.Grind.CommRing.Mon → Lean.Expr → M Lean.Expr
-- Mathlib.Order.SymmDiff
symmDiff_left_comm : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b c : α), symmDiff a (symmDiff b c) = symmDiff b (symmDiff a c)
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.notMem_of_mem_sdiff_closure`. -/
Matroid.notMem_of_mem_diff_closure : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e : α}, e ∈ M.E \ M.closure X → e ∉ X
-- Init.Data.BitVec.Lemmas
BitVec.eq_sub_iff_add_eq : ∀ {w : ℕ} {x y z : BitVec w}, x = z - y ↔ x + y = z
-- Mathlib.AlgebraicGeometry.Fiber
/-- `f.fiberι y : f.fiber y ⟶ X` is the embedding of the scheme-theoretic fiber into `X`.  -/
AlgebraicGeometry.Scheme.Hom.fiberι : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → (y : ↥Y) → AlgebraicGeometry.Scheme.Hom.fiber f y ⟶ X
-- Mathlib.FieldTheory.KummerExtension
X_pow_mul_sub_C_irreducible : ∀ {K : Type u} [inst : Field K] {n m : ℕ} {a : K},
  Irreducible (Polynomial.X ^ m - Polynomial.C a) →
    (∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
        minpoly K x = Polynomial.X ^ m - Polynomial.C a →
          Irreducible (Polynomial.X ^ n - Polynomial.C (IntermediateField.AdjoinSimple.gen K x))) →
      Irreducible (Polynomial.X ^ (n * m) - Polynomial.C a)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.uniformContinuous_toCloseds : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T2Space α],
  UniformContinuous TopologicalSpace.NonemptyCompacts.toCloseds
-- Mathlib.Order.Antichain
IsWeakAntichain.subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] {s t : Set ((i : ι) → α i)},
  IsWeakAntichain s → t ⊆ s → IsWeakAntichain t
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.algHom_ext'_iff : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : CommSemiring k] {A : Type u_3} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k]
  {φ₁ φ₂ : SkewMonoidAlgebra k G →ₐ[k] A},
  φ₁ = φ₂ ↔ (↑φ₁).comp (SkewMonoidAlgebra.of k G) = (↑φ₂).comp (SkewMonoidAlgebra.of k G)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.isInteriorPoint_disjointUnion_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_5} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {p : M ⊕ M'},
  I.IsInteriorPoint p → ∀ (hleft : p.isLeft = true), I.IsInteriorPoint (p.getLeft hleft)
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_zero_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ), ProbabilityTheory.Kernel.compProd 0 κ = 0
-- Mathlib.Algebra.Lie.UniversalEnveloping
UniversalEnvelopingAlgebra.ι_apply : ∀ (R : Type u₁) {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x : L),
  (UniversalEnvelopingAlgebra.ι R) x = (UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)
-- Mathlib.Topology.Covering.Basic
IsOpen.trivializationDiscrete_target : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X}
  [inst_2 : Nonempty (X → E)] {ι : Type u_3} [inst_3 : Nonempty ι] [inst_4 : TopologicalSpace ι]
  [inst_5 : DiscreteTopology ι] (U : ι → Set E) (V : Set X) (open_V : IsOpen V)
  (open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen W ↔ IsOpen (f ⁻¹' W ∩ U i))) (inj : ∀ (i : ι), Set.InjOn f (U i))
  (surj : ∀ (i : ι), Set.SurjOn f (U i) V) (disjoint : Pairwise (Function.onFun Disjoint U))
  (exhaustive : f ⁻¹' V ⊆ ⋃ i, U i),
  (IsOpen.trivializationDiscrete U V open_V open_iff inj surj disjoint exhaustive).target = V ×ˢ Set.univ
-- Mathlib.Data.Set.Lattice
Set.biInter_union : ∀ {α : Type u_1} {β : Type u_2} (s t : Set α) (u : α → Set β), ⋂ x ∈ s ∪ t, u x = (⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
/-- The Dirichlet convolution of two arithmetic functions `f` and `g` is another arithmetic function
such that `(f * g) n` is the sum of `f x * g y` over all `(x,y)` such that `x * y = n`.  -/
ArithmeticFunction.instMul : {R : Type u_1} → [inst : Semiring R] → Mul (ArithmeticFunction R)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arccos_eq_arctan : ∀ {x : ℝ}, 0 < x → Real.arccos x = Real.arctan (√(1 - x ^ 2) / x)
-- Mathlib.Analysis.Convex.Star
starConvex_iInter₂ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E} {ι : Sort u_4} {κ : ι → Sort u_5} {s : (i : ι) → κ i → Set E},
  (∀ (i : ι) (j : κ i), StarConvex 𝕜 x (s i j)) → StarConvex 𝕜 x (⋂ i, ⋂ j, s i j)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.swapRight_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)), κ.swapRight = κ.map Prod.swap
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_eq_getD_keysArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {fallback : α}, t.minKeyD fallback = t.keysArray.getD 0 fallback
-- Mathlib.Topology.Algebra.Group.Basic
/-- A version of `Pi.continuousNeg` for non-dependent functions. It is needed
because sometimes Lean fails to use `Pi.continuousNeg` for non-dependent functions.  -/
Pi.has_continuous_neg' : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [ContinuousNeg G] {ι : Type u_1}, ContinuousNeg (ι → G)
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_sumElim : ∀ {ι₁ : Type u_12} {ι₂ : Type u_13} {α : Type u_14} {M : Type u_15} [inst : Zero α] [inst_1 : AddCommMonoid M]
  (f₁ : ι₁ →₀ α) (f₂ : ι₂ →₀ α) (g : ι₁ ⊕ ι₂ → α → M),
  (f₁.sumElim f₂).sum g = f₁.sum (g ∘ Sum.inl) + f₂.sum (g ∘ Sum.inr)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesAt.differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E}, HasFPowerSeriesAt f p x → DifferentiableAt 𝕜 f x
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_def : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1) (r : k),
  AffineMap.homothety c r = r • (AffineMap.id k P1 -ᵥ AffineMap.const k P1 c) +ᵥ AffineMap.const k P1 c
-- Mathlib.Order.Interval.Set.LinearOrder
/-- **Alias** of `Set.Ici_sdiff_Ioi`. -/
Set.Ici_diff_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ici a \ Set.Ioi b = Set.Icc a b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β] {f : Option β → Option β},
  Std.DTreeMap.Const.get! (Std.DTreeMap.Const.alter t k f) k = (f (Std.DTreeMap.Const.get? t k)).get!
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ \ m₂).getKey? k = none