mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_17.splitter : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (x y : CategoryTheory.WithInitial Cᵒᵖ) → (x ⟶ y) → Sort u_3) →
      (x y : CategoryTheory.WithInitial Cᵒᵖ) →
        (f : x ⟶ y) →
          ((x y : C) →
              (f : CategoryTheory.WithInitial.of (Opposite.op x) ⟶ CategoryTheory.WithInitial.of (Opposite.op y)) →
                motive (CategoryTheory.WithInitial.of (Opposite.op x)) (CategoryTheory.WithInitial.of (Opposite.op y))
                  f) →
            ((unop : C) →
                (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of (Opposite.op unop)) →
                  motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of (Opposite.op unop)) x) →
              ((x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
                  motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x) →
                motive x y f
-- Mathlib.Tactic.CancelDenoms.Core
/-- `cancel_denoms` attempts to remove numerals from the denominators of fractions.
It works on propositions that are field-valued inequalities.

```lean
variable [LinearOrderedField α] (a b c : α)

example (h : a / 5 + b / 4 < c) : 4*a + 5*b < 20*c := by
  cancel_denoms at h
  exact h

example (h : a > 0) : a / 5 > 0 := by
  cancel_denoms
  exact h
```
 -/
Mathlib.Tactic.cancelDenoms : Lean.ParserDescr
-- Init.Control.Lawful.Instances
ExceptT.instLawfulMonad : ∀ {m : Type u_1 → Type u_2} {ε : Type u_1} [inst : Monad m] [LawfulMonad m], LawfulMonad (ExceptT ε m)
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForILeansParams.mk.injEq : ∀ (uri? : Option Lean.Lsp.DocumentUri) (version? : Option ℕ) (uri?_1 : Option Lean.Lsp.DocumentUri)
  (version?_1 : Option ℕ),
  ({ uri? := uri?, version? := version? } = { uri? := uri?_1, version? := version?_1 }) =
    (uri? = uri?_1 ∧ version? = version?_1)
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fdiv.match_1.eq_4 : ∀ (motive : ℤ → ℤ → Sort u_1) (a : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (a : ℕ) → motive (Int.negSucc a) 0) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_6 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc a, 0 with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc a, 0 => h_4 a
    | Int.negSucc m, Int.ofNat n.succ => h_5 m n
    | Int.negSucc m, Int.negSucc n => h_6 m n) =
    h_4 a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.insert k v)[k]? = some v
-- Mathlib.Geometry.Manifold.BumpFunction
/-- If `f` is a smooth bump function and `s` closed subset of the support of `f` (i.e., of the open
ball of radius `f.rOut`), then there exists `0 < r < f.rOut` such that `s` is a subset of the open
ball of radius `r`. Formally, `s ⊆ e.source ∩ e ⁻¹' (ball (e c) r)`, where `e = extChartAt I c`.  -/
SmoothBumpFunction.exists_r_pos_lt_subset_ball : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E] {s : Set M},
  IsClosed s →
    s ⊆ Function.support ↑f →
      ∃ r ∈ Set.Ioo 0 f.rOut, s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' Metric.ball (↑(extChartAt I c) c) r
-- Lean.Data.KVMap
Lean.KVMap.subsetAux : List (Lean.Name × Lean.DataValue) → Lean.KVMap → Bool
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.IsometryEquiv.prodComm_invFun : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (a : M₂ × M₁),
  (QuadraticMap.IsometryEquiv.prodComm Q₁ Q₂).invFun a = a.swap
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.trans : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y z : α}, f.SameCycle x y → f.SameCycle y z → f.SameCycle x z
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instForInProdOfMonad : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → {m : Type u_1 → Type u_2} → [Monad m] → ForIn m (RBTree.RBMap α β cmp) (α × β)
-- Mathlib.Analysis.Normed.Module.DoubleDual
/-- `inclusionInDoubleDualWeak` is a topological embedding from the weak topology to the weak-star
topology.  -/
NormedSpace.isEmbedding_inclusionInDoubleDualWeak : ∀ (𝕜 : Type u_3) [inst : RCLike 𝕜] (X : Type u_4) [inst_1 : NormedAddCommGroup X] [inst_2 : NormedSpace 𝕜 X],
  Topology.IsEmbedding ⇑(NormedSpace.inclusionInDoubleDualWeak 𝕜 X)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.subtractionCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionCommMonoid α],
  Finset.subtractionCommMonoid = Function.Injective.subtractionCommMonoid SetLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_functor_obj_ι_app_star : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {t : CategoryTheory.Limits.Cocone K},
  (CategoryTheory.WithInitial.coconeEquiv.functor.obj t).ι.app CategoryTheory.WithInitial.star = t.pt.hom
-- Mathlib.Data.ENNReal.Operations
ENNReal.Ico_eq_Iio : ∀ {y : ENNReal}, Set.Ico 0 y = Set.Iio y
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.FindAux.mk : {n : ℕ} → (s : Array Batteries.UFNode) → Fin n → s.size = n → Batteries.UnionFind.FindAux n
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.instPartialOrder.eq_1 : ∀ {G : Type u_1} [inst : Group G], Subgroup.instPartialOrder = PartialOrder.ofSetLike (Subgroup G) G
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} (self : F.HomObj G A) {c d : C} (f : c ⟶ d)
  (a : A.obj c),
  CategoryTheory.CategoryStruct.comp (F.map f) (self.app d ((CategoryTheory.ConcreteCategory.hom (A.map f)) a)) =
    CategoryTheory.CategoryStruct.comp (self.app c a) (G.map f)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.Monic.pow : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R} {n : ℕ},
  m.Monic f → m.Monic (f ^ n)
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.continuousAt_iff' : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β] {f : β → α} {b : β},
  ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhds b, edist (f x) (f b) < ε
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {fallback v : β}, (t.insertIfNew k v).getD a fallback = if cmp k a = Ordering.eq ∧ k ∉ t then v else t.getD a fallback
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousOn.nnnorm' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {s : Set α},
  ContinuousOn f s → ContinuousOn (fun x => ‖f x‖₊) s
-- Mathlib.Geometry.Euclidean.Triangle
/-- Given a triangle `ABC` with `A ≠ B` and `A ≠ C` and a point `P` on `BC`,
`∠ B A P + ∠ P A C = ∠ B A C`.  -/
EuclideanGeometry.angle_add_of_ne_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c p : P},
  a ≠ b →
    a ≠ c → Wbtw ℝ b p c → EuclideanGeometry.angle b a p + EuclideanGeometry.angle p a c = EuclideanGeometry.angle b a c
-- Mathlib.Data.List.Basic
List.map_surjective_iff : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Surjective (List.map f) ↔ Function.Surjective f
-- Mathlib.NumberTheory.Pell
/-- If we multiply a positive solution with the inverse of a fundamental solution,
the `x`-coordinate stays positive.  -/
Pell.IsFundamental.mul_inv_x_pos : ∀ {d : ℤ} {a₁ : Pell.Solution₁ d},
  Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → 0 < a.y → 0 < (a * a₁⁻¹).x
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.exists_root : ∀ {k : Type u} [inst : Field k] [IsSepClosed k] (p : Polynomial k), p.degree ≠ 0 → p.Separable → ∃ x, p.IsRoot x
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.leadingCoeff_map : ∀ {R : Type u} {S : Type v} [inst : Ring R] [IsSimpleRing R] [inst_2 : Semiring S] [Nontrivial S] {p : Polynomial R}
  (f : R →+* S), (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
/-- A recapitulation of the definition of multiplicative that is simpler for proofs  -/
ArithmeticFunction.IsMultiplicative.iff_ne_zero : ∀ {R : Type u_1} [inst : MonoidWithZero R] {f : ArithmeticFunction R},
  f.IsMultiplicative ↔ f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
-- Lean.Meta.Constructions.SparseCasesOn
Lean.Meta.SparseCasesOnInfo.mk.sizeOf_spec : ∀ (indName : Lean.Name) (majorPos arity : ℕ) (insterestingCtors : Array Lean.Name),
  sizeOf { indName := indName, majorPos := majorPos, arity := arity, insterestingCtors := insterestingCtors } =
    1 + sizeOf indName + sizeOf majorPos + sizeOf arity + sizeOf insterestingCtors
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- If
```
  P --fst--> X
  |          |
 snd         f
  |          |
  v          v
  Y ---g---> Z

```
is a pullback square and `g` is an open immersion, then the stalk map induced by `snd` at `p`
is isomorphic to the stalk map of `f` at `fst p`.
 -/
AlgebraicGeometry.Scheme.stalkMapIsoOfIsPullback : {P X Y Z : AlgebraicGeometry.Scheme} →
  {fst : P ⟶ X} →
    {snd : P ⟶ Y} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          CategoryTheory.IsPullback fst snd f g →
            [AlgebraicGeometry.IsOpenImmersion g] →
              (p : ↥P) →
                (x : optParam (↥X) (fst p)) →
                  autoParam (fst p = x) AlgebraicGeometry.Scheme.stalkMapIsoOfIsPullback._auto_1 →
                    (CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap f x) ≅
                      CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap snd p))
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.comp_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂)
  (g : sq₂.Hom sq₃), (f.comp g).τ₁ = CategoryTheory.CategoryStruct.comp f.τ₁ g.τ₁
-- Mathlib.Algebra.Polynomial.Eval.SMul
Polynomial.eval₂_smul : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (g : R →+* S) (p : Polynomial R) (x : S) {s : R},
  Polynomial.eval₂ g x (s • p) = g s * Polynomial.eval₂ g x p
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
RCLike.intervalIntegral_ofReal : ∀ {𝕜 : Type u_8} [inst : RCLike 𝕜] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℝ},
  ∫ (x : ℝ) in a..b, ↑(f x) ∂μ = ↑(∫ (x : ℝ) in a..b, f x ∂μ)
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_mem_smul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  {I : Submodule R A} {N : Submodule R M} {r : A} {n : M}, r ∈ I → n ∈ N → r • n ∈ I • N
-- Init.Data.List.Lemmas
List.getLastD_concat : ∀ {α : Type u_1} {a b : α} {l : List α}, (l ++ [b]).getLastD a = b
-- Init.Data.Array.Find
Array.find?_append : ∀ {α : Type u_1} {p : α → Bool} {xs ys : Array α}, Array.find? p (xs ++ ys) = (Array.find? p xs).or (Array.find? p ys)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {X Y : C} {f : X ⟶ Y}
  [inst_5 : SizeOf C] [inst_6 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W x)] [inst_7 : SizeOf J]
  (toTransfiniteCompositionOfShape : CategoryTheory.TransfiniteCompositionOfShape J f)
  (map_mem : ∀ (j : J), ¬IsMax j → W (toTransfiniteCompositionOfShape.F.map (CategoryTheory.homOfLE ⋯))),
  sizeOf { toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape, map_mem := map_mem } =
    1 + sizeOf toTransfiniteCompositionOfShape
-- Lean.Server.CodeActions.Basic
_private.Lean.Server.CodeActions.Basic.0.Lean.Server.builtinCodeActionProviders : IO.Ref (Lean.NameMap Lean.Server.CodeActionProvider)
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.id_map : ∀ {X : CategoryTheory.ReflQuiv} {x y : ↑X} (f : x ⟶ y), (CategoryTheory.CategoryStruct.id X).map f = f
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_smul : ∀ {R : Type u_3} [inst : CommRing R] (r : R) (q : Quaternion R), Quaternion.normSq (r • q) = r ^ 2 * Quaternion.normSq q
-- Std.Data.HashMap.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.HashMap.modify : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → (β → β) → Std.HashMap α β
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.comp_fderivWithin : ∀ {𝕜 : 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] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G},
  UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (⇑iso ∘ f) s x = ↑↑iso ∘SL fderivWithin 𝕜 f s x
-- Mathlib.Topology.Algebra.Group.Basic
OrderDual.instIsTopologicalGroup : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G], IsTopologicalGroup Gᵒᵈ
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sectR_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (a : α), ProbabilityTheory.Kernel.sectR 0 a = 0
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_self : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a / a = 1
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.shift_ι_map_ιK_assoc : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} A] {ι : CategoryTheory.Functor A C} {X₁ : A} {X₃ : C}
  (f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)) {K : A}
  (α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃) [inst_3 : ι.Full] {Z : C}
  (h : (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C 1).map (ι.map (CategoryTheory.Triangulated.AbelianSubcategory.ιK f₃ α))) h =
    CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp f₃ h)
-- Mathlib.Data.Seq.Computation
Computation.lmap.eq_2 : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (val : γ), Computation.lmap f (Sum.inr val) = Sum.inr val
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- Lifts a function `R → posSubmonoid R → α` to the value group-with-zero of `R`.  -/
ValuativeRel.ValueGroupWithZero.lift : {R : Type u_1} →
  [inst : Semiring R] →
    [inst_1 : ValuativeRel R] →
      {α : Sort u_2} →
        (f : R → ↥(ValuativeRel.posSubmonoid R) → α) →
          (∀ (x y : R) (t s : ↥(ValuativeRel.posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) →
            ValuativeRel.ValueGroupWithZero R → α
-- Std.Time.Time.PlainTime
/-- Subtracts minutes from a `PlainTime`.
 -/
Std.Time.PlainTime.subMinutes : Std.Time.PlainTime → Std.Time.Minute.Offset → Std.Time.PlainTime
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_isLink : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (E₀ : Set β) (e : β) (x y : α),
  (G.restrict E₀).IsLink e x y = (e ∈ E₀ ∧ G.IsLink e x y)
-- Mathlib.RingTheory.Discriminant
/-- A variation of `Algebra.discr_powerBasis_eq_prod`.  -/
Algebra.discr_powerBasis_eq_prod'' : ∀ (K : Type u) {L : Type v} (E : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Field E] [inst_3 : Algebra K L]
  [inst_4 : Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) [Algebra.IsSeparable K L]
  (e : Fin pb.dim ≃ (L →ₐ[K] E)),
  (algebraMap K E) (Algebra.discr K ⇑pb.basis) =
    (-1) ^ (Module.finrank K L * (Module.finrank K L - 1) / 2) *
      ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)
-- Mathlib.Topology.Closure
IsOpen.inter_frontier_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → s ∩ frontier s = ∅
-- Init.Data.Int.DivMod.Basic
/-- Integer modulus using the F-rounding convention.

In the F-rounding convention (flooring division), `Int.fdiv x y` satisfies `Int.fdiv x y = ⌊x / y⌋`
and `Int.fmod` is the unique function satisfying `Int.fmod x y + (Int.fdiv x y) * y = x`.

Examples:

* `(7 : Int).fmod (0 : Int) = 7`
* `(0 : Int).fmod (7 : Int) = 0`

* `(12 : Int).fmod (6 : Int) = 0`
* `(12 : Int).fmod (-6 : Int) = 0`
* `(-12 : Int).fmod (6 : Int) = 0`
* `(-12 : Int).fmod (-6 : Int) = 0`

* `(12 : Int).fmod (7 : Int) = 5`
* `(12 : Int).fmod (-7 : Int) = -2`
* `(-12 : Int).fmod (7 : Int) = 2`
* `(-12 : Int).fmod (-7 : Int) = -5`

 -/
Int.fmod : ℤ → ℤ → ℤ
-- Mathlib.CategoryTheory.Products.Basic
/-- The equivalence of categories between `(A ⥤ B) × (A ⥤ C)` and `A ⥤ (B × C)`  -/
CategoryTheory.functorProdFunctorEquiv : (A : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    (B : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        (C : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            CategoryTheory.Functor A B × CategoryTheory.Functor A C ≌ CategoryTheory.Functor A (B × C)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`.  -/
EuclideanGeometry.oangle_right_eq_arctan_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
    EuclideanGeometry.oangle p₂ p₃ p₁ = ↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂))
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term_add_term : ∀ {α : Type u_1} [inst : AddCommMonoid α] (n₁ : ℕ) (x a₁ : α) (n₂ : ℕ) (a₂ : α) (n' : ℕ) (a' : α),
  n₁ + n₂ = n' →
    a₁ + a₂ = a' →
      Mathlib.Tactic.Abel.term n₁ x a₁ + Mathlib.Tactic.Abel.term n₂ x a₂ = Mathlib.Tactic.Abel.term n' x a'
-- Mathlib.Algebra.GroupWithZero.Defs
MulZeroOneClass.toMulOneClass : {M₀ : Type u} → [self : MulZeroOneClass M₀] → MulOneClass M₀
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd_add_zero_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A) (X : C),
  (CategoryTheory.shiftFunctorAdd C a 0).hom.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      ((CategoryTheory.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C a).obj X))
-- Mathlib.CategoryTheory.GuitartExact.Quotient
CategoryTheory.TwoSquare.GuitartExact.quotient_of_nonempty_rightHomotopy : ∀ {C₀ : Type u_1} {C : Type u_2} {H₀ : Type u_3} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} H₀]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} H] {T : CategoryTheory.Functor C₀ H₀} {L : CategoryTheory.Functor C₀ C}
  {R : CategoryTheory.Functor H₀ H} {B : CategoryTheory.Functor C H} [T.EssSurj] [T.Full] [B.Full]
  (e : T.comp R ≅ L.comp B),
  (∀ ⦃X : C⦄ ⦃Y₀ : C₀⦄ (f₀ f₁ : X ⟶ L.obj Y₀),
      B.map f₀ = B.map f₁ → ∃ P, T.map P.p₀ = T.map P.p₁ ∧ Nonempty ((P.map L).RightHomotopy f₀ f₁)) →
    CategoryTheory.TwoSquare.GuitartExact e.inv
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.prevn.eq_def : ∀ (x : Substring.Raw) (x_1 : ℕ) (x_2 : String.Pos.Raw),
  x.prevn x_1 x_2 =
    match x, x_1, x_2 with
    | x, 0, p => p
    | ss, i.succ, p => ss.prevn i (ss.prev p)
-- Lean.Parser.Term
Lean.Parser.Term.ident.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : SizeOf C] (toFunctor : CategoryTheory.Functor C C)
  (η : CategoryTheory.Functor.id C ⟶ toFunctor) (μ : toFunctor.comp toFunctor ⟶ toFunctor)
  (assoc :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toFunctor.map (μ.app X)) (μ.app X) =
          CategoryTheory.CategoryStruct.comp (μ.app (toFunctor.obj X)) (μ.app X))
      CategoryTheory.Monad.assoc._autoParam)
  (left_unit :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (η.app (toFunctor.obj X)) (μ.app X) =
          CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj (toFunctor.obj X)))
      CategoryTheory.Monad.left_unit._autoParam)
  (right_unit :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toFunctor.map (η.app X)) (μ.app X) =
          CategoryTheory.CategoryStruct.id (toFunctor.obj ((CategoryTheory.Functor.id C).obj X)))
      CategoryTheory.Monad.right_unit._autoParam),
  sizeOf { toFunctor := toFunctor, η := η, μ := μ, assoc := assoc, left_unit := left_unit, right_unit := right_unit } =
    1 + sizeOf toFunctor + sizeOf η + sizeOf μ
-- Mathlib.Order.Comparable
compRel_comm : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, CompRel r a b ↔ CompRel r b a
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.eq_3 : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (k : ℤ)
  (a : Lean.Grind.Linarith.Expr), Lean.Grind.Linarith.Expr.denoteN ctx (Lean.Grind.Linarith.Expr.intMul k a) = 0
-- Mathlib.Logic.Equiv.Defs
Equiv.ofBijective_apply_symm_apply : ∀ {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) (x : β), f ((Equiv.ofBijective f hf).symm x) = x
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.toSphere.instIsOpenPosMeasure : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsOpenPosMeasure], μ.toSphere.IsOpenPosMeasure
-- Std.Do.WP.Basic
Std.Do.Reader.instWP : {ρ : Type u_1} → Std.Do.WP (ReaderM ρ) (Std.Do.PostShape.arg ρ Std.Do.PostShape.pure)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.Monic.mul : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.Monic f → m.Monic g → m.Monic (f * g)
-- Mathlib.Order.GaloisConnection.Basic
isGLB_image2_of_isGLB_isLUB : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {s : Set α}
  {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β},
  (∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) →
    (∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) →
      IsGLB s a₀ → IsLUB t b₀ → IsGLB (Set.image2 u s t) (u a₀ b₀)