mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.shortAddLong.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2],
  RootPairing.EmbeddedG2.shortAddLong P =
    (P.reflectionPerm (RootPairing.EmbeddedG2.long P)) (RootPairing.EmbeddedG2.short P)
-- Init.Prelude
instMinNat : Min ℕ
-- Mathlib.Algebra.Group.InjSurj
/-- A type has left-cancellative addition, if it admits an injective map that
preserves `+` to another type with left-cancellative addition.  -/
Function.Injective.isLeftCancelAdd : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Add M₂] [IsLeftCancelAdd M₂] (f : M₁ → M₂),
  Function.Injective f → (∀ (x y : M₁), f (x + y) = f x + f y) → IsLeftCancelAdd M₁
-- Mathlib.Data.Finset.Basic
List.toFinset_filter : ∀ {α : Type u_1} [inst : DecidableEq α] (s : List α) (p : α → Bool),
  (List.filter p s).toFinset = {x ∈ s.toFinset | p x = true}
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.horn_ι_mem_innerHornInclusions : ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → SSet.innerHornInclusions (SSet.horn n i).ι
-- Mathlib.GroupTheory.FiniteAbelian.Basic
Subgroup.isFiniteRelIndex_map_powMonoidHom_of_fg : ∀ {A : Type u_1} [inst : CommGroup A] {B : Subgroup A},
  B.FG → ∀ {n : ℕ}, n ≠ 0 → (Subgroup.map (powMonoidHom n) B).IsFiniteRelIndex B
-- Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
/-- **Integration by parts for line derivatives**
Version with a general bilinear form `B`.
If `B f g` is integrable, as well as `B f' g` and `B f g'` where `f'` and `g'` are derivatives
of `f` and `g` in a given direction `v`, then `∫ B f g' = - ∫ B f' g`.  -/
integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} {W : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  [inst_6 : NormedAddCommGroup W] [inst_7 : NormedSpace ℝ W] [inst_8 : MeasurableSpace E] {μ : MeasureTheory.Measure E}
  [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {f f' : E → F} {g g' : E → G} {v : E}
  {B : F →L[ℝ] G →L[ℝ] W},
  MeasureTheory.Integrable (fun x => (B (f' x)) (g x)) μ →
    MeasureTheory.Integrable (fun x => (B (f x)) (g' x)) μ →
      MeasureTheory.Integrable (fun x => (B (f x)) (g x)) μ →
        (∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v) →
          (∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v) →
            ∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
-- Init.Data.BitVec.Basic
BitVec.instHashable : {n : ℕ} → Hashable (BitVec n)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.instInhabitedPriority.default : Aesop.Frontend.Priority
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β), f.comp (OrderRingHom.id α) = f
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
isLinearSet_iff_exists_fin_addMonoidHom : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, IsLinearSet s ↔ ∃ a n f, s = a +ᵥ Set.range ⇑f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_add_nat_mul_two_pi : ∀ (x : ℝ) (n : ℕ), Real.sin (x + ↑n * (2 * Real.pi)) = Real.sin x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The cochain complex of homomorphisms between two cochain complexes `F` and `G`.
In degree `n : ℤ`, it consists of the abelian group `HomComplex.Cochain F G n`.  -/
CochainComplex.HomComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CochainComplex C ℤ → CochainComplex C ℤ → CochainComplex AddCommGrpCat ℤ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceEq : Lean.Meta.Simp.Simproc
-- Init.Data.Vector.Lemmas
Vector.map_eq_flatMap : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n},
  Vector.map f xs = Vector.cast ⋯ (xs.flatMap fun x => #v[f x])
-- Mathlib.SetTheory.ZFC.Basic
/-- The set difference operation  -/
ZFSet.diff : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}
-- Mathlib.Data.Ordmap.Ordset
Ordnode.map.valid : ∀ {α : Type u_1} [inst : Preorder α] {β : Type u_2} [inst_1 : Preorder β] {f : α → β},
  StrictMono f → ∀ {t : Ordnode α}, t.Valid → (Ordnode.map f t).Valid
-- Mathlib.CategoryTheory.Limits.Creates
/-- When `F` is fully faithful, to show that `F` creates the colimit for `K` it suffices to exhibit a
lift of a colimit cocone for `K ⋙ F`.
 -/
CategoryTheory.createsColimitOfFullyFaithfulOfLift' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.Full] →
                  [F.Faithful] →
                    {l : CategoryTheory.Limits.Cocone (K.comp F)} →
                      CategoryTheory.Limits.IsColimit l →
                        (c : CategoryTheory.Limits.Cocone K) → (F.mapCocone c ≅ l) → CategoryTheory.CreatesColimit K F
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of a commutative magma by a congruence relation is a commutative magma.  -/
Con.commMagma : {M : Type u_4} → [inst : CommMagma M] → (c : Con M) → CommMagma c.Quotient
-- Mathlib.Logic.Equiv.Fin.Rotate
finRotate_symm_apply : ∀ {n : ℕ} (i : Fin n), (Equiv.symm (finRotate n)) i = i - 1
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Category.{max u v, max u v} (CategoryTheory.Factorisation f)
-- Mathlib.Algebra.Group.Hom.Instances
/-- `OneHom M N` is a `CommMonoid` if `N` is commutative.  -/
OneHom.instCommMonoid : {M : Type uM} → {N : Type uN} → [inst : One M] → [inst_1 : CommMonoid N] → CommMonoid (OneHom M N)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.all_eq_false_iff_exists_contains_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  {p : α → β → Bool},
  m.WF → (m.all p = false ↔ ∃ a, ∃ (h : m.contains a = true), p a (Std.DHashMap.Raw.Const.get m a h) = false)
-- Mathlib.Algebra.Group.Basic
add_eq_zero_iff_eq_neg : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a + b = 0 ↔ a = -b
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_eval₂ : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  (f : R →+* S₁) (g : S₂ → MvPolynomial S₃ R) (p : MvPolynomial S₂ R),
  (MvPolynomial.map f) (MvPolynomial.eval₂ MvPolynomial.C g p) =
    MvPolynomial.eval₂ MvPolynomial.C (⇑(MvPolynomial.map f) ∘ g) ((MvPolynomial.map f) p)
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.integral_comp : ∀ {E' : Type u_2} {F' : Type u_3} {A : Type u_4} [inst : NormedAddCommGroup E'] [inst_1 : InnerProductSpace ℝ E']
  [inst_2 : FiniteDimensional ℝ E'] [inst_3 : MeasurableSpace E'] [inst_4 : BorelSpace E']
  [inst_5 : NormedAddCommGroup F'] [inst_6 : InnerProductSpace ℝ F'] [inst_7 : FiniteDimensional ℝ F']
  [inst_8 : MeasurableSpace F'] [inst_9 : BorelSpace F'] (f : E' ≃ₗᵢ[ℝ] F') [inst_10 : NormedAddCommGroup A]
  [inst_11 : NormedSpace ℝ A] (g : F' → A), ∫ (x : E'), g (f x) = ∫ (y : F'), g y
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).get k h' = m₂.get k ⋯
-- Mathlib.Data.ZMod.Defs
Fin.val_intCast : ∀ {n : ℕ} [inst : NeZero n] (x : ℤ), ↑↑x = (x % ↑n).toNat
-- Mathlib.LinearAlgebra.LinearPMap
/-- Compose two `LinearPMap`s  -/
LinearPMap.comp : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : Ring R] →
        [inst_1 : Ring S] →
          [inst_2 : Ring T] →
            {σ : R →+* S} →
              {τ : S →+* T} →
                {E : Type u_4} →
                  [inst_3 : AddCommGroup E] →
                    [inst_4 : Module R E] →
                      {F : Type u_5} →
                        [inst_5 : AddCommGroup F] →
                          [inst_6 : Module S F] →
                            {G : Type u_6} →
                              [inst_7 : AddCommGroup G] →
                                [inst_8 : Module T G] →
                                  {ρ : R →+* T} →
                                    [RingHomCompTriple σ τ ρ] →
                                      (g : F →ₛₗ.[τ] G) →
                                        (f : E →ₛₗ.[σ] F) → (∀ (x : ↥f.domain), ↑f x ∈ g.domain) → E →ₛₗ.[ρ] G
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  ∃ a ∈ ↑I,
    a ≠ 0 ∧
      ↑|(Algebra.norm ℚ) a| ≤
        ↑(FractionalIdeal.absNorm ↑I) * (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
              ↑(Module.finrank ℚ K).factorial /
            ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K *
          √|↑(NumberField.discr K)|
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.coe_snd : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N], ⇑(AddMonoidHom.snd M N) = Prod.snd
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.State.mk.inj : ∀ {exp : ℕ} {rings : Array Lean.Meta.Sym.Arith.CommRing} {semirings : Array Lean.Meta.Sym.Arith.CommSemiring}
  {ncRings : Array Lean.Meta.Sym.Arith.Ring} {ncSemirings : Array Lean.Meta.Sym.Arith.Semiring}
  {typeClassify : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.Arith.ClassifyResult} {exp_1 : ℕ}
  {rings_1 : Array Lean.Meta.Sym.Arith.CommRing} {semirings_1 : Array Lean.Meta.Sym.Arith.CommSemiring}
  {ncRings_1 : Array Lean.Meta.Sym.Arith.Ring} {ncSemirings_1 : Array Lean.Meta.Sym.Arith.Semiring}
  {typeClassify_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.Arith.ClassifyResult},
  { exp := exp, rings := rings, semirings := semirings, ncRings := ncRings, ncSemirings := ncSemirings,
        typeClassify := typeClassify } =
      { exp := exp_1, rings := rings_1, semirings := semirings_1, ncRings := ncRings_1, ncSemirings := ncSemirings_1,
        typeClassify := typeClassify_1 } →
    exp = exp_1 ∧
      rings = rings_1 ∧
        semirings = semirings_1 ∧ ncRings = ncRings_1 ∧ ncSemirings = ncSemirings_1 ∧ typeClassify = typeClassify_1
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
/-- Define the fixed point as the quotient of trees under the equivalence relation.
 -/
MvQPF.wSetoid : {n : ℕ} → {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → (α : TypeVec.{u} n) → Setoid ((MvQPF.P F).W α)
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
/-- The conditional cdf is lower or equal to 1 for all `a : α`.  -/
ProbabilityTheory.condCDF_le_one : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (x : ℝ),
  ↑(ProbabilityTheory.condCDF ρ a) x ≤ 1
-- Mathlib.CategoryTheory.Monad.Coequalizer
CategoryTheory.Monad.beckAlgebraCofork_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra),
  (CategoryTheory.Monad.beckAlgebraCofork X).pt = X
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.abs_dvd : ∀ {a p : ℤ}, a ∣ p → Int.Internal.Linear.abs a ∣ p
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.State.mk : ℕ →
  Array Lean.Meta.Sym.Arith.CommRing →
    Array Lean.Meta.Sym.Arith.CommSemiring →
      Array Lean.Meta.Sym.Arith.Ring →
        Array Lean.Meta.Sym.Arith.Semiring →
          Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.Arith.ClassifyResult → Lean.Meta.Sym.Arith.State
-- Batteries.Lean.NameMapAttribute
/-- Environment extension that maps declaration names to `α`.
This uses a `Thunk` to avoid computing the name map when it isn't used.  -/
Lean.NameMapExtension : Type → Type
-- Mathlib.Analysis.Normed.Group.Constructions
pi_norm_le_iff_of_nonempty' : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i)
  {r : ℝ} [Nonempty ι], ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
-- Mathlib.AlgebraicGeometry.SpreadingOut
/-- Let `x : X` and `f g : X ⟶ Y` be two morphisms such that `f x = g x`.
If `f` and `g` agree on the stalk of `x`, then they agree on an open neighborhood of `x`,
provided `X` is "germ-injective" at `x` (e.g. when it's integral or locally Noetherian).

TODO: The condition on `X` is unnecessary when `Y` is locally of finite type.
 -/
AlgebraicGeometry.spread_out_unique_of_isGermInjective : ∀ {X Y : AlgebraicGeometry.Scheme} {x : ↥X} [X.IsGermInjectiveAt x] (f g : X ⟶ Y) (e : f x = g x),
  AlgebraicGeometry.Scheme.Hom.stalkMap f x =
      CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (AlgebraicGeometry.Scheme.Hom.stalkMap g x) →
    ∃ U, x ∈ U ∧ CategoryTheory.CategoryStruct.comp U.ι f = CategoryTheory.CategoryStruct.comp U.ι g
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.coe_pow : ∀ {S : Type u_1} {R : Type u_2} [inst : Mul R] [inst_1 : Add R] [inst_2 : Star R] [inst_3 : SMul S R] (f : R ≃⋆ₐ[S] R)
  (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.foldr_eq_foldr_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {δ : Type w} {f : α → δ → δ} {init : δ},
  Std.TreeSet.Raw.foldr f init t = Array.foldr f init t.toArray
-- Mathlib.Analysis.Asymptotics.Completion
_private.Mathlib.Analysis.Asymptotics.Completion.0.«term_̂» : Lean.TrailingParserDescr
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- **Alias** of `ContMDiff.curry_right`.

---

Curried `C^n` functions are `C^n` in the second coordinate.  -/
ContMDiff.along_snd : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {x : M},
  ContMDiff (I.prod I') J n (Function.uncurry f) → ContMDiff I' J n fun y => f x y
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomInvPair.toRingEquiv_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] (σ : R₁ →+* R₂) (σ' : R₂ →+* R₁)
  [inst_2 : RingHomInvPair σ σ'] (a : R₁), (RingHomInvPair.toRingEquiv σ σ') a = σ a
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.coyonedaLemma.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.coyonedaLemma C =
    CategoryTheory.NatIso.ofComponents (fun x => (CategoryTheory.coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.findM?_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  [LawfulMonad m] [Std.Iterators.Finite α m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {f : β → m (ULift.{w, 0} Bool)},
  it.findM? f = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => do
        let __do_lift ← f out
        if __do_lift.down = true then pure (some out) else it'.findM? f
      | Std.IterStep.skip it' => it'.findM? f
      | Std.IterStep.done => pure none
-- Mathlib.Order.InitialSeg
PrincipalSeg.transInitial_top : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  (f : PrincipalSeg r s) (g : InitialSeg s t), (f.transInitial g).top = g f.top
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapRangeAlgAut_apply : ∀ (R : Type u_1) {A : Type u_4} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (f : A ≃ₐ[R] A), (MonoidAlgebra.mapRangeAlgAut R M) f = MonoidAlgebra.mapAlgEquiv R M f
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
/-- If `P` implies being an open map, the by `P` induced precoverage is coarser
than the quasi-compact precoverage.  -/
AlgebraicGeometry.Scheme.precoverage_le_qcPrecoverage_of_isOpenMap : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  (P ≤ fun x x_1 f => IsOpenMap ⇑f) → AlgebraicGeometry.Scheme.precoverage P ≤ AlgebraicGeometry.Scheme.qcPrecoverage
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualAnnihilator_dualAnnihilator_eq : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] (W : Subspace K V),
  (Submodule.dualAnnihilator W).dualAnnihilator = (Module.mapEvalEquiv K V) W
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- Evaluation of a Mahler series is just the pointwise sum.  -/
PadicInt.mahlerSeries_apply : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] {a : ℕ → E},
  Filter.Tendsto a Filter.atTop (nhds 0) → ∀ (x : ℤ_[p]), (PadicInt.mahlerSeries a) x = ∑' (n : ℕ), (mahler n) x • a n
-- Mathlib.Analysis.Real.OfDigits
Real.ofDigitsTerm_le : ∀ {b : ℕ} {digits : ℕ → Fin b} {n : ℕ}, Real.ofDigitsTerm digits n ≤ (↑b - 1) * (↑b ^ (n + 1))⁻¹
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom.brecOn.eq : ∀ {B : Type u} [inst : Quiver B] {motive : (a a_1 : B) → CategoryTheory.FreeBicategory.Hom a a_1 → Sort u_1} {a a_1 : B}
  (t : CategoryTheory.FreeBicategory.Hom a a_1)
  (F_1 :
    (a a_2 : B) →
      (t : CategoryTheory.FreeBicategory.Hom a a_2) → CategoryTheory.FreeBicategory.Hom.below t → motive a a_2 t),
  CategoryTheory.FreeBicategory.Hom.brecOn t F_1 = F_1 a a_1 t (CategoryTheory.FreeBicategory.Hom.brecOn.go t F_1).2
-- Mathlib.Combinatorics.Graph.Basic
Graph.isLink_self_iff : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.IsLink e x x ↔ G.IsLoopAt e x
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle_obj₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁],
  (CategoryTheory.Pretriangulated.productTriangle T).obj₁ = ∏ᶜ fun j => (T j).obj₁
-- Mathlib.NumberTheory.Bernoulli
bernoulli_zero : bernoulli 0 = 1
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.IsStronglyConnected.nonempty_path : ∀ (V : Type u_2) [inst : Quiver V], Quiver.IsStronglyConnected V → ∀ (i j : V), Nonempty (Quiver.Path i j)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSets.bInter : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)} {s' : Set (Set Ω)}
  {u : Set ι},
  (∃ n ∈ u, ProbabilityTheory.CondIndepSets m' hm' (s n) s' μ) →
    ProbabilityTheory.CondIndepSets m' hm' (⋂ n ∈ u, s n) s' μ
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instDivisionMonoid : {α : Type u_1} → [DivisionMonoid α] → DivisionMonoid αᵐᵒᵖ
-- Mathlib.Topology.Algebra.Group.Defs
IsTopologicalGroup.to_continuousDiv : ∀ {G : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G], ContinuousDiv G
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mem_toNonUnitalSubsemiring : ∀ {R : Type u} [inst : NonAssocSemiring R] {S : Subsemiring R} {x : R}, x ∈ S.toNonUnitalSubsemiring ↔ x ∈ S
-- Mathlib.Topology.MetricSpace.Defs
instMetricSpaceOrderDual : {X : Type u_1} → [MetricSpace X] → MetricSpace Xᵒᵈ
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.fun_vadd : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {𝕜 : Type u_5} [inst_1 : TopologicalSpace 𝕜] [inst_2 : VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α → 𝕜} {g : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun i => f i +ᵥ g i) μ
-- Mathlib.Data.Rat.Cast.Defs
eq_nnratCast : ∀ {F : Type u_1} {α : Type u_3} [inst : DivisionSemiring α] [inst_1 : FunLike F ℚ≥0 α] [RingHomClass F ℚ≥0 α] (f : F)
  (q : ℚ≥0), f q = ↑q
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_nat_mod : ∀ (l : List ℕ) (n : ℕ), l.prod % n = (List.map (fun x => x % n) l).prod % n
-- Mathlib.Data.Real.Embedding
Archimedean.ratLt'.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : One M] (x : M),
  Archimedean.ratLt' x = ⇑(Rat.castHom ℝ) '' Archimedean.ratLt x
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.initCore : Lean.MVarId → Lean.Meta.Grind.GrindM Lean.Meta.Grind.Goal
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.cells_subset_iff : ∀ {μ ν : YoungDiagram}, μ.cells ⊆ ν.cells ↔ μ ≤ ν
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x : β),
  CauSeq.Completion.ofRat (-x) = -CauSeq.Completion.ofRat x
-- Mathlib.GroupTheory.Schreier
AddSubgroup.exists_finset_card_le_add : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [H.FiniteIndex] {S : Finset G},
  AddSubgroup.closure ↑S = ⊤ → ∃ T, T.card ≤ H.index * S.card ∧ AddSubgroup.closure ↑T = ⊤
-- Init.Data.Array.Erase
Array.eraseP_map : ∀ {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {xs : Array β},
  (Array.map f xs).eraseP p = Array.map f (xs.eraseP (p ∘ f))
-- Std.Internal.UV.System
/-- Information about the current group,
 -/
Std.Internal.UV.System.GroupInfo : Type
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.IsSeparated (CategoryTheory.CategoryStruct.comp f g)], AlgebraicGeometry.IsSeparated f
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsUpper.isTopologicalSpace_basis : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] [t : TopologicalSpace α] [Topology.IsUpper α] (U : Set α),
  IsOpen U ↔ U = Set.univ ∨ ∃ a, (Set.Iic a)ᶜ = U
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Any morphism from a terminal object is split mono.  -/
CategoryTheory.Limits.IsTerminal.isSplitMono_from : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsTerminal X)
  (f : X ⟶ Y), CategoryTheory.IsSplitMono f
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Preserves addition.  -/
AddEquivClass.map_add : ∀ {F : Type u_9} {A : outParam (Type u_10)} {B : outParam (Type u_11)} {inst : Add A} {inst_1 : Add B}
  {inst_2 : EquivLike F A B} [self : AddEquivClass F A B] (f : F) (a b : A), f (a + b) = f a + f b