mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.associated_isOrtho : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {Q : QuadraticMap R M N} [inst_5 : Invertible 2] {x y : M},
  ((QuadraticMap.associated Q) x) y = 0 ↔ Q.IsOrtho x y
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_ne_zero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M} [Nontrivial M], UniqueFactorizationMonoid.radical a ≠ 0
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum' : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (g⁻¹ • x) ∂μ
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.δ_shift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a m : ℤ),
  CochainComplex.HomComplex.δ n m (γ.shift a) = a.negOnePow • (CochainComplex.HomComplex.δ n m γ).shift a
-- Init.Data.Iterators.Consumers.Loop
/-- Returns `true` if the iterator yields no values.

`O(|it|)` since the iterator may skip an unknown number of times before returning a result.
Short-circuits upon encountering the first result. Only the first element of `it` is examined.

If the iterator is not productive, this function might run forever. The variant
`it.ensureTermination.isEmpty` always terminates after finitely many steps.

Examples:
* `[].iter.isEmpty = true`
* `[1].iter.isEmpty = false`
 -/
Std.Iter.isEmpty : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter β → Bool
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get?_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ \ t₂).get? k = if k ∈ t₂ then none else t₁.get? k
-- Mathlib.Combinatorics.Matroid.Basic
/-- create a copy of `M : Matroid α` with an independence predicate and ground set defeq
to supplied arguments that are provably equal to those of `M`.  -/
Matroid.copyIndep : {α : Type u_1} →
  (M : Matroid α) → (E : Set α) → (Indep : Set α → Prop) → E = M.E → (∀ (I : Set α), Indep I ↔ M.Indep I) → Matroid α
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- The boundary natural transformation of a `HomologyPretheory`.  -/
TopPair.HomologyPretheory.δ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (self : TopPair.HomologyPretheory C c) → (i j : ι) → self.Hₚ i ⟶ TopPair.proj₂.comp (self.H j)
-- Mathlib.Data.List.GetD
List.getI_cons_succ : ∀ {α : Type u} (x : α) (xs : List α) (n : ℕ) [inst : Inhabited α], (x :: xs).getI (n + 1) = xs.getI n
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mcasesPat%_» : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.abs_intervalIntegral_eq : ∀ (f : ℝ → ℝ) (a b : ℝ) (μ : MeasureTheory.Measure ℝ), |∫ (x : ℝ) in a..b, f x ∂μ| = |∫ (x : ℝ) in Set.uIoc a b, f x ∂μ|
-- Mathlib.Algebra.Module.Torsion.Basic
_private.Mathlib.Algebra.Module.Torsion.Basic.0.Submodule.disjoint_torsionBySet_ideal.match_1_1.eq_1 : ∀ (motive : Fin 2 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Implementation; see `nonempty_indParallelPairPresentation`.  -/
CategoryTheory.NonemptyParallelPairPresentationAux.presentation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      (f g : A ⟶ B) →
        CategoryTheory.Limits.IndObjectPresentation A →
          CategoryTheory.Limits.IndObjectPresentation B → CategoryTheory.IndParallelPairPresentation f g
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.integrable_comp_div_left : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : Group G] [MeasurableMul G] [MeasurableInv G] (f : G → F) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G),
  MeasureTheory.Integrable (fun t => f (g / t)) μ ↔ MeasureTheory.Integrable f μ
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.eraseListₘ.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (hd : α)
  (tl : List α), m.eraseListₘ (hd :: tl) = (m.erase hd).eraseListₘ tl
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_comm : ∀ {α : Type u_1} {f g : Equiv.Perm α}, f.Disjoint g ↔ g.Disjoint f
-- Mathlib.Algebra.Group.Defs
add_sub_assoc : ∀ {G : Type u_1} [inst : SubNegMonoid G] (a b c : G), a + b - c = a + (b - c)
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.hasDerivWithinAt_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R 𝕜]
  (q : Polynomial R) (x : 𝕜) (s : Set 𝕜),
  HasDerivWithinAt (fun x => (Polynomial.aeval x) q) ((Polynomial.aeval x) (Polynomial.derivative q)) s x
-- Init.Prelude
/-- Transforms exceptions with a function, doing nothing on successful results.
 -/
EStateM.adaptExcept : {ε σ α ε' : Type u} → (ε → ε') → EStateM ε σ α → EStateM ε' σ α
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.toRatVec_nonneg : ∀ {ι : Type u_3} (x : ι → ℕ), 0 ≤ toRatVec✝ x
-- Init.Data.Array.Lemmas
Array.toList_eq_nil_iff : ∀ {α : Type u_1} {xs : Array α}, xs.toList = [] ↔ xs = #[]
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.ext_iff : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} {φ ψ : ρ.Equiv σ}, φ = ψ ↔ ⇑φ = ⇑ψ
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.integrable_continuousLinearMap_prod : ∀ {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {mE : MeasurableSpace E} [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {mF : MeasurableSpace F}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.Measure E}
  [MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure F} [MeasureTheory.IsProbabilityMeasure ν]
  {L : E × F →L[ℝ] G},
  MeasureTheory.Integrable id μ → MeasureTheory.Integrable id ν → MeasureTheory.Integrable (⇑L) (μ.prod ν)
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.flippingIso_inv_toFunctor_obj_obj_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (k : C) (j : D),
  ((CategoryTheory.flippingIso.inv.toFunctor.obj F).obj k).obj j = (F.obj j).obj k
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- In the model space, any element of the groupoid is in the maximal atlas.  -/
StructureGroupoid.mem_maximalAtlas_of_mem_groupoid : ∀ {H : Type u} [inst : TopologicalSpace H] (G : StructureGroupoid H) {f : OpenPartialHomeomorph H H},
  f ∈ G → f ∈ StructureGroupoid.maximalAtlas H G
-- Std.Time.Format
/-- The leanDateTimeWithZone format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ`
for representing date, time, and time zone. It uses the default value that can be parsed with the
notation of dates.
 -/
Std.Time.Formats.leanDateTimeWithZone : Std.Time.GenericFormat Std.Time.Awareness.any
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_inter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.Const.get! (m₁.inter! m₂) k =
          if Std.DTreeMap.Internal.Impl.contains k m₂ = true then Std.DTreeMap.Internal.Impl.Const.get! m₁ k
          else default
-- Mathlib.NumberTheory.Harmonic.Bounds
harmonic.eq_1 : ∀ (n : ℕ), harmonic n = ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹
-- Init.Data.UInt.Bitwise
UInt16.ofNatLT_and : ∀ (a b : ℕ) (ha : a < 2 ^ 16) (hb : b < 2 ^ 16),
  UInt16.ofNatLT (a &&& b) ⋯ = UInt16.ofNatLT a ha &&& UInt16.ofNatLT b hb
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- `n.succ`-pretransitivity implies `n`-preprimitivity.  -/
MulAction.isMultiplyPreprimitive_of_isMultiplyPretransitive_succ : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {n : ℕ},
  ↑n.succ ≤ ENat.card α → ∀ [MulAction.IsMultiplyPretransitive M α n.succ], MulAction.IsMultiplyPreprimitive M α n
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- Dirac measure considered as a tempered distribution is the delta distribution.  -/
TemperedDistribution.toTemperedDistribution_dirac_eq_delta : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : SecondCountableTopology E] (x : E),
  (MeasureTheory.Measure.dirac x).toTemperedDistribution = TemperedDistribution.delta x
-- Mathlib.Data.ENNReal.BigOperators
/-- A product of finite numbers is still finite.  -/
ENNReal.prod_lt_top : ∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal}, (∀ a ∈ s, f a < ⊤) → ∏ a ∈ s, f a < ⊤
-- Mathlib.Analysis.Seminorm
/-- Seminorm-balls containing the origin are absorbent.  -/
Seminorm.absorbent_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {r : ℝ} {x : E}, p x < r → Absorbent 𝕜 (p.ball x r)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α} [inst_3 : Inhabited (β k)],
      (List.map Sigma.fst l).contains k = false → (t.insertMany l).get! k = t.get! k
-- Mathlib.Algebra.Ring.Parity
Odd.add_even : ∀ {α : Type u_2} [inst : Semiring α] {a b : α}, Odd a → Even b → Odd (a + b)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : x.Balanced) (x_2 : ℕ) (x_3 : x_2 < x.size),
  x.keyAtIdx x_1 x_2 x_3 =
    match x, x_1, x_2, x_3 with
    | Std.DTreeMap.Internal.Impl.inner size k v l' r', hl, n, h =>
      match h_1 : compare n l'.size with
      | Ordering.lt => l'.keyAtIdx ⋯ n ⋯
      | Ordering.eq => k
      | Ordering.gt => r'.keyAtIdx ⋯ (n - l'.size - 1) ⋯
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_algebra_tower'`. -/
Ideal.ramificationIdx_algebra_tower' : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [IsScalarTower R S T] [IsDedekindDomain S]
  [IsDedekindDomain T] [IsDomain R] [Module.IsTorsionFree R S] [Module.IsTorsionFree S T] (p : Ideal R) (P : Ideal S)
  (Q : Ideal T) [Q.IsPrime] [Q.LiesOver P] [P.LiesOver p],
  p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q
-- Mathlib.Order.CompleteBooleanAlgebra
CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq : ∀ {α : Type u} [inst : CompleteLattice α],
  CompletelyDistribLattice.MinimalAxioms α →
    ∀ {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_iff_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m.contains a = true ↔ a ∈ m
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_toList_rco : ∀ {m n : ℤ}, (m...n).toList.toArray = (m...n).toArray
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a functor `F` preserves the right homology of a short complex `S`, this is the
canonical isomorphism `(S.map F).rightHomology ≅ F.obj S.rightHomology`.  -/
CategoryTheory.ShortComplex.mapRightHomologyIso : {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.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (S : CategoryTheory.ShortComplex C) →
              (F : CategoryTheory.Functor C D) →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : S.HasRightHomology] →
                    [inst_6 : F.PreservesRightHomologyOf S] → (S.map F).rightHomology ≅ F.obj S.rightHomology
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.mono_pushout_of_mono_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Mono f],
  CategoryTheory.Mono (CategoryTheory.Limits.pushout.inr f g)
-- Init.Grind.ToInt
/-- The embedding into the integers takes numerals in the range interval to themselves.
 -/
Lean.Grind.ToInt.OfNat : (α : Type u) → [(n : ℕ) → OfNat α n] → (I : outParam Lean.Grind.IntInterval) → [Lean.Grind.ToInt α I] → Prop
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.dualAnnihilator_eq_bot_iff' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {W : Submodule R M},
  W.dualAnnihilator = ⊥ ↔ Subsingleton (Module.Dual R (M ⧸ W))
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ofPointIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit r)
  [i : CategoryTheory.IsIso (P.desc t)],
  P.ofPointIso = P.ofIsoColimit (CategoryTheory.asIso' (P.descCoconeMorphism t)).symm
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len w : ℕ} (aig : Std.Sat.AIG α)
  (oldLayer : aig.RefVec (len * w)) (h : 0 < len),
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go oldLayer h).aig.decls.size
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.measurePreserving_neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Neg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G)
  [μ.IsNegInvariant], MeasureTheory.MeasurePreserving Neg.neg μ μ
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Module.of_apply : ∀ (R : Type u_1) (ι : Type u_2) [inst : Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Semiring R]
  [inst_5 : (i : ι) → AddCommMonoid (G i)] [inst_6 : (i : ι) → Module R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] (i : ι) (x : G i),
  (DirectLimit.Module.of R ι G f i) x = ⟦⟨i, x⟩⟧
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_id : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N : LieSubmodule R L M}, LieSubmodule.map LieModuleHom.id N = N
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- The difference between the characteristic functions for the poles of `f` and `f - const` simplifies
to the difference between the proximity functions.
 -/
ValueDistribution.characteristic_sub_characteristic_eq_proximity_sub_proximity : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
  Meromorphic f →
    ∀ (a₀ : E),
      ValueDistribution.characteristic f ⊤ - ValueDistribution.characteristic (fun x => f x - a₀) ⊤ =
        ValueDistribution.proximity f ⊤ - ValueDistribution.proximity (fun x => f x - a₀) ⊤
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofDocInfo : Lean.Elab.DocInfo → Lean.Elab.Info
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- **Alias** of `GradedAlgHom.restrictScalars_toAlgHom`. -/
GradedAlgHom.restrictScalars_coe_algHom : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] (R₀ : Type u_11)
  [inst_9 : CommSemiring R₀] [inst_10 : Algebra R₀ R] [inst_11 : Algebra R₀ A] [inst_12 : Algebra R₀ B]
  [inst_13 : IsScalarTower R₀ R A] [inst_14 : IsScalarTower R₀ R B] (f : 𝒜 →ₐᵍ[R] ℬ),
  AlgHom.restrictScalars R₀ ↑f = ↑(↑R₀ f)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_eq_iSup_genEigenspace_nat : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R) (k : ℕ∞), (f.genEigenspace μ) k = ⨆ l, (f.genEigenspace μ) ↑↑l
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- A word and its maximal reduction correspond to the same element of the free group.  -/
FreeGroup.reduce.self : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α], FreeGroup.mk (FreeGroup.reduce L) = FreeGroup.mk L
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.mul_mul_conjTranspose_same : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : Fintype n] [inst_4 : Fintype m] {A : Matrix n n R} {B : Matrix m n R},
  A.PosDef → (Function.Injective fun v => Matrix.vecMul v B) → (B * A * B.conjTranspose).PosDef
-- Init.Data.Float.Float
/-- Computes the tangent of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`tan`.
 -/
Float.tan : Float → Float
-- Mathlib.Computability.Primrec.Basic
PrimrecPred.decide : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop} [inst_1 : DecidablePred p],
  PrimrecPred p → Primrec fun a => decide (p a)
-- Mathlib.Data.Tree.Basic
BinaryTree.numLeaves.eq_2 : ∀ {α : Type u} (a : α) (l r : BinaryTree α), (BinaryTree.node a l r).numLeaves = l.numLeaves + r.numLeaves
-- Std.Time.Date.Unit.Month
Std.Time.Month.instLEOffset : LE Std.Time.Month.Offset
-- Mathlib.SetTheory.Cardinal.Regular
Ordinal.preOmega_univ : Ordinal.preOmega Ordinal.univ.{u, v} = Ordinal.univ.{u, v}
-- Mathlib.RingTheory.AdjoinRoot
/-- Let `α` have minimal polynomial `f` over `R` and `I` be an ideal of `R`,
then `R[α] / (I) = (R[x] / (f)) / pS = (R/p)[x] / (f mod p)`.  -/
PowerBasis.quotientEquivQuotientMinpolyMap : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (pb : PowerBasis R S) →
            (I : Ideal R) →
              (S ⧸ Ideal.map (algebraMap R S) I) ≃ₐ[R]
                Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_neg_I : ∀ {K : Type u_1} [inst : RCLike K], (starRingEnd K) (-RCLike.I) = RCLike.I
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Context.ref : Lean.Elab.Term.Do.ToCodeBlock.Context → Lean.Syntax
-- Std.Sync.SharedMutex
Std.instNonemptyBaseSharedMutex : Nonempty Std.BaseSharedMutex
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_univ_right : ∀ {G : Type u_1} [inst : Group G] {S : Set G}, Subgroup.IsComplement S Set.univ ↔ ∃ g, S = {g}
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.map_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : Y}, x ∈ e.target → ↑e.symm x ∈ e.source
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Cfg.inhabited : {Γ : Type u_1} → {Λ : Type u_2} → [Inhabited Λ] → [inst : Inhabited Γ] → Inhabited (Turing.TM0.Cfg Γ Λ)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {ι : Type v}
  (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) (AlgebraicGeometry.SheafedSpace C))
  [inst_2 : CategoryTheory.Limits.HasColimit F] (i : CategoryTheory.Discrete ι),
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i).hom.base)
-- Mathlib.Tactic.Sat.FromLRAT
/-- The `v` variable under the `a1 ... an, v, h1 ... hn` context  -/
Mathlib.Tactic.Sat.buildReify.v : ℕ → Lean.Expr
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.ofMulEquivOfLocalizations_eq_iff_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {k : N ≃* P} {x : M} {y : P},
  (f.ofMulEquivOfLocalizations k) x = y ↔ f x = k.symm y
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : (a : α) → β a → γ a} {k : α}
  {h' : k ∈ Std.DHashMap.Raw.map f m} (h : m.WF), (Std.DHashMap.Raw.map f m).getKey k h' = m.getKey k ⋯
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.continuousAt_add_coe_bot : ∀ (a : ℝ), ContinuousAt (fun p => p.1 + p.2) (↑a, ⊥)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.isMulCommutative : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → Mul (f i)] [∀ (i : I), IsMulCommutative (f i)],
  IsMulCommutative ((i : I) → f i)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalNatExprCore : Lean.Expr → Lean.MetaM ℕ
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.RankLeOneStruct.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] [inst_2 : SizeOf R]
  (emb : ValuativeRel.ValueGroupWithZero R →*₀ NNReal) (strictMono : StrictMono ⇑emb),
  sizeOf { emb := emb, strictMono := strictMono } = 1 + sizeOf emb
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.upper_two_blockTriangular : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} {R : Type v} [inst : Zero R] [inst_1 : Preorder α] (A : Matrix m m R)
  (B : Matrix m n R) (D : Matrix n n R) {a b : α},
  a < b → (Matrix.fromBlocks A B 0 D).BlockTriangular (Sum.elim (fun x => a) fun x => b)
-- Std.Data.ExtHashMap.Lemmas
_private.Std.Data.ExtHashMap.Lemmas.0.GetElem?.match_1.splitter : (elem : outParam (Type u_1)) →
  (motive : Option elem → Sort u_2) →
    (x : Option elem) → ((e : elem) → motive (some e)) → (Unit → motive none) → motive x
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
_private.Mathlib.Data.Nat.Factorial.DoubleFactorial.0.Nat.factorial.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 ()
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.eqOnSource_iff : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e' : OpenPartialHomeomorph X Y), e.EqOnSource e' ↔ e.EqOnSource e'.toPartialEquiv
-- Mathlib.Algebra.Ring.Int.Parity
/-- **Alias** of `Int.even_xor_odd'`. -/
Int.even_xor'_odd' : ∀ (n : ℤ), ∃ k, Xor (n = 2 * k) (n = 2 * k + 1)