mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.splits_minpoly : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [n : Normal K L]
  (c : ConjRootClass K L), (Polynomial.map (algebraMap K L) c.minpoly).Splits
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- If homology has finite rank support contained in a finite set,
the `finsum` homological Euler characteristic equals the finite sum over that set.  -/
HomologicalComplex.homologyEulerChar_eq_sum_finSet_of_finrankSupport_subset : ∀ {R : Type u_1} [inst : Ring R] {ι : Type u_2} {c : ComplexShape ι} [inst_1 : c.EulerCharSigns]
  (C : HomologicalComplex (ModuleCat R) c) [inst_2 : ∀ (i : ι), C.HasHomology i] (indices : Finset ι),
  (GradedObject.finrankSupport fun i => C.homology i) ⊆ ↑indices →
    C.homologyEulerChar = ∑ i ∈ indices, ↑(c.χ i) * ↑(Module.finrank R ↑(C.homology i))
-- Init.Data.Int.Basic
/-- The integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
 -/
Int : Type
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (h : Diffeomorph I I' M M' n) {s : Set M} {x : M}, ContMDiffWithinAt I I' n (⇑h) s x
-- Mathlib.Data.Finsupp.SMulWithZero
Finsupp.smulZeroClass : {α : Type u_1} → {M : Type u_5} → {R : Type u_11} → [inst : Zero M] → [SMulZeroClass R M] → SMulZeroClass R (α →₀ M)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.power_le_aleph0 : ∀ {a b : Cardinal.{u}}, a ≤ Cardinal.aleph0 → b < Cardinal.aleph0 → a ^ b ≤ Cardinal.aleph0
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The unit of the multiplication is `single 1 1`,
i.e. the function that is `1` at `1` and `0` elsewhere.  -/
MonoidAlgebra.one : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [One M] → One (MonoidAlgebra R M)
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.category : CategoryTheory.Category.{u_1, u_1 + 1} AlexDisc
-- Std.Async.Signal
Std.Async.Signal.sigprof.sizeOf_spec : sizeOf Std.Async.Signal.sigprof = 1
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- If `p` splits in `F` then the `p.gal` is trivial.  -/
Polynomial.Gal.uniqueGalOfSplits : {F : Type u_1} → [inst : Field F] → (p : Polynomial F) → p.Splits → Unique p.Gal
-- Init.Data.String.Length
_private.Init.Data.String.Length.0.Nat.repeat.match_1.eq_2 : ∀ {α : Type u_2} (motive : ℕ → α → Sort u_1) (n : ℕ) (a : α) (h_1 : (a : α) → motive 0 a)
  (h_2 : (n : ℕ) → (a : α) → motive n.succ a),
  (match n.succ, a with
    | 0, a => h_1 a
    | n.succ, a => h_2 n a) =
    h_2 n a
-- Mathlib.Algebra.Tropical.Basic
Tropical.instPartialOrderTropical : {R : Type u} → [PartialOrder R] → PartialOrder (Tropical R)
-- Lean.Parser.Command
Lean.Parser.Command.derivingClasses.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Control.Bitraversable.Basic
/-- Bifunctor. This typeclass asserts that a lawless bitraversable bifunctor is lawful.  -/
LawfulBitraversable : (t : Type u → Type u → Type u) → [Bitraversable t] → Prop
-- Mathlib.Algebra.QuaternionBasis
/-- The second imaginary unit  -/
QuaternionAlgebra.Basis.j : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] → [inst_2 : Algebra R A] → {c₁ c₂ c₃ : R} → QuaternionAlgebra.Basis A c₁ c₂ c₃ → A
-- Mathlib.Algebra.Group.Opposite
MulOpposite.op_pow : ∀ {α : Type u_1} [inst : Monoid α] (x : α) (n : ℕ), MulOpposite.op (x ^ n) = MulOpposite.op x ^ n
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- The `transpose` of a Young diagram is obtained by swapping i's with j's.  -/
YoungDiagram.transpose : YoungDiagram → YoungDiagram
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis.exchange : ∀ {α : Type u_1} {M : Matroid α} {I X J : Set α} {e : α},
  M.IsBasis I X → M.IsBasis J X → e ∈ I \ J → ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows_comp_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {σ : Type u_2} {Y : ι → C}
  (f : (i : ι) → Y i ⟶ X) (a : σ → ι),
  (CategoryTheory.Presieve.ofArrows (Y ∘ a) fun i => f (a i)) ≤ CategoryTheory.Presieve.ofArrows Y f
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_one_left : ∀ (x : Ordinal.{u_1}), Ordinal.log 1 x = 0
-- Mathlib.Algebra.Homology.TotalComplex
/-- The total complex of a bicomplex.  -/
HomologicalComplex₂.total : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {I₁₂ : Type u_4} →
            {c₁ : ComplexShape I₁} →
              {c₂ : ComplexShape I₂} →
                (K : HomologicalComplex₂ C c₁ c₂) →
                  (c₁₂ : ComplexShape I₁₂) →
                    [inst_2 : TotalComplexShape c₁ c₂ c₁₂] →
                      [DecidableEq I₁₂] → [K.HasTotal c₁₂] → HomologicalComplex C c₁₂
-- Init.Prelude
instMonadFunctorTOfMonadFunctor : (m : Type u_1 → Type u_2) →
  (n : Type u_1 → Type u_3) → (o : Type u_1 → Type u_4) → [MonadFunctor n o] → [MonadFunctorT m n] → MonadFunctorT m o
-- Mathlib.Algebra.BigOperators.Expect
Finset.smul_expect : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {G : Type u_6}
  [inst_2 : DistribSMul G M] [SMulCommClass G ℚ≥0 M] (a : G) (s : Finset ι) (f : ι → M),
  (a • s.expect fun i => f i) = s.expect fun i => a • f i
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.mk_toWord : ∀ {α : Type u_1} [inst : DecidableEq α] {x : FreeGroup α}, FreeGroup.mk x.toWord = x
-- Mathlib.Algebra.Group.Finsupp
AddEquiv.finsuppUnique_symm_apply_apply : ∀ {M : Type u_3} [inst : AddZeroClass M] {ι : Type u_8} [inst_1 : Unique ι] (a : M) (a_1 : ι),
  (AddEquiv.finsuppUnique.symm a) a_1 = a
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.piTensorHomMapFun₂.eq_1 : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} {t' : ι → Type u_12} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] [inst_5 : (i : ι) → AddCommMonoid (t' i)] [inst_6 : (i : ι) → Module R (t' i)]
  (φ : PiTensorProduct R fun i => s i →ₗ[R] t i →ₗ[R] t' i),
  φ.piTensorHomMapFun₂ =
    PiTensorProduct.lift
      (PiTensorProduct.piTensorHomMap.compMultilinearMap
        ((PiTensorProduct.lift (MultilinearMap.piLinearMap (PiTensorProduct.tprod R))) φ))
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_comap_lift : ∀ {α : Type u} {β : Type v} (M : Matroid β) (f : α → β) (X : Set α),
  Cardinal.lift.{v, u} ((M.comap f).cRk X) = Cardinal.lift.{u, v} (M.cRk (f '' X))
-- Mathlib.ModelTheory.Definability
Set.definable_iUnion_of_finite : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {ι : Type u_2} [Finite ι]
  {f : ι → Set (α → M)}, (∀ (i : ι), A.Definable L (f i)) → A.Definable L (⋃ i, f i)
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- The junk value when `𝔸` can't be equipped with a `ℚ`-algebra structure.  -/
NormedSpace.exp_of_isEmpty_algebra_rat : ∀ {𝔸 : Type u_2} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] [IsEmpty (Algebra ℚ 𝔸)]
  (x : 𝔸), NormedSpace.exp x = 1
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.cast_eq_cast : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {i j : ℕ}
  (h : i = j), ⇑(TensorPower.cast R M h) = cast ⋯
-- Init.Grind.Order
Lean.Grind.Order.le_of_offset_eq_1_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b : α} {k : ℤ}, a = b + ↑k → a ≤ b + ↑k
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_f_fst_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + 1 = q)
  {Z : C} (h : F.X q ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
      (CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v p q hpq) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Init.Data.String.Lemmas.Iterate
String.Slice.Model.mem_positionsFrom : ∀ {s : String.Slice} {p : s.Pos} {q : { q // q ≠ s.endPos }}, q ∈ String.Slice.Model.positionsFrom p ↔ p ≤ ↑q
-- Aesop.Search.SearchM
Aesop.SearchM.instInhabitedState.default : {Q : Type} → {inst : Aesop.Queue Q} → [Inhabited Q] → Aesop.SearchM.State Q
-- Mathlib.Order.Partition.Basic
Partition.partOf_subset : ∀ {α : Type u_1} {x : α} {u : Set α} {P : Partition u}, P.partOf x ⊆ u
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.instHasPullbacksRefineOneHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X)
  [inst_1 : E.HasPullbacks]
  (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))),
  (E.refineOneHypercover F).HasPullbacks
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Overlap.nonzero.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)}
  [inst : (a : Q(«$α»)) → SizeOf (bt a)]
  (x : Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExProd bt sα) e),
  sizeOf (Mathlib.Tactic.Ring.Common.Overlap.nonzero x) = 1 + sizeOf x
-- Mathlib.Order.RelClasses
Order.Preimage.instIsPreorder : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [IsPreorder α r] {f : β → α}, IsPreorder β (f ⁻¹'o r)
-- Init.Data.Nat.Basic
Nat.le_of_lt_add_one : ∀ {n m : ℕ}, n < m + 1 → n ≤ m
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_uIcc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a b : α} [OrderClosedTopology α], MeasurableSet (Set.uIcc a b)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vaddAssocClass' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α β] [inst_1 : VAdd α γ] [inst_2 : VAdd β γ]
  [VAddAssocClass α β γ], VAddAssocClass α (Set β) (Set γ)
-- Mathlib.Algebra.Order.Group.Synonym
isLeftRegular_toColex : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, IsLeftRegular (toColex a) ↔ IsLeftRegular a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_dblU : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).dblU (⇑f ∘ P) = f (W'.dblU P)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_union_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
  (contains_right : Std.DTreeMap.Internal.Impl.contains k m₂ = true),
  (m₁.union m₂ ⋯ ⋯).get k ⋯ = m₂.get k contains_right
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.distribLattice : {V : Type u} → {G : SimpleGraph V} → DistribLattice G.Subgraph
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_le_mk_add_of_archimedean : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {S : Type u_3}
  [inst_3 : LinearOrder S] [inst_4 : CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) (x : R) (y : S),
  ArchimedeanClass.mk x ≤ ArchimedeanClass.mk (f y) + ArchimedeanClass.mk x
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.hom_ext : ∀ {R S : RingCat} {f g : R ⟶ S}, RingCat.Hom.hom f = RingCat.Hom.hom g → f = g
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
CategoryTheory.Nerve.instIsCoskeletalNerveOfNatNat : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.SimplicialObject.IsCoskeletal (CategoryTheory.nerve C) 2
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.exists_mem : ∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β}, f =ᶠ[l] g → ∃ s ∈ l, Set.EqOn f g s
-- Mathlib.Data.Fin.Fin2
Fin2.brecOn.eq : ∀ {motive : (a : ℕ) → Fin2 a → Sort u} {a : ℕ} (t : Fin2 a) (F_1 : (a : ℕ) → (t : Fin2 a) → Fin2.below t → motive a t),
  Fin2.brecOn t F_1 = F_1 a t (Fin2.brecOn.go t F_1).2
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Truncated.tensor_map_apply_snd : ∀ {n : ℕ} {X Y : SSet.Truncated n} {d e : (SimplexCategory.Truncated n)ᵒᵖ} (f : d ⟶ e)
  (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj d),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (X.map f) (Y.map f))) x).2 =
    (CategoryTheory.ConcreteCategory.hom (Y.map f)) x.2
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.evalEval_polynomial : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} (x y : R),
  Polynomial.evalEval x y W.polynomial = y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)
-- Init.Data.Nat.Lemmas
Nat.min_eq_zero_iff : ∀ {m n : ℕ}, min m n = 0 ↔ m = 0 ∨ n = 0
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.GuessLexRel.no_idea.sizeOf_spec : sizeOf Lean.Elab.WF.GuessLex.GuessLexRel.no_idea = 1
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_comp_σ_succ'_assoc : ∀ {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.succ →
    ∀ {Z : SimplexCategory} (h : { len := n } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) h) =
        h
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.inhabited : {α : Type u} → Inhabited { s // s.Finite }
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_monadMap_StateT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ : Type u}
  (f : {β : Type u} → m β → m β) {α : Type u} (x : StateT σ m α) (post : α → σ → Pred) (epost : EPred),
  Std.Internal.Do.wp (MonadFunctor.monadMap (fun {β} => f) x) post epost = fun s =>
    Std.Internal.Do.wp (f (x.run s))
      (fun x =>
        match x with
        | (a, s') => post a s')
      epost
-- Mathlib.MeasureTheory.Group.Arithmetic
List.measurable_prod : ∀ {M : Type u_2} {α : Type u_3} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} (l : List (α → M)), (∀ f ∈ l, Measurable f) → Measurable l.prod
-- Lean.Meta.DiscrTree.Main
/-- Similar to `getMatch`, but returns solutions that are prefixes of `e`.
We store the number of ignored arguments in the result. -/
Lean.Meta.DiscrTree.getMatchWithExtra : {α : Type} → Lean.Meta.DiscrTree α → Lean.Expr → Lean.MetaM (Array (α × ℕ))
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.small_pos_neg_pos_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] {A : Finset G} {K : ℝ},
  ↑(A ^ 3).card ≤ K * ↑A.card → ↑(A * A⁻¹ * A).card ≤ K ^ 3 * ↑A.card
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_monotone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X),
  Monotone (CategoryTheory.Sieve.pullback f)
-- Mathlib.Topology.UniformSpace.Cauchy
DiscreteUniformity.eq_pure_cauchyConst : ∀ {α : Type u} [uniformSpace : UniformSpace α] [inst : DiscreteUniformity α] {f : Filter α} (hf : Cauchy f),
  f = pure (DiscreteUniformity.cauchyConst hf)
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- Send a measure `ν` on `Y` and a function `f` on `X × Y` to the function on `X` given by
`x ↦ ν (f (x, ·))`, or more suggestively, `x ↦ ∫ f(x, y) dμ(y)`.  -/
AbstractMeasure.contractSnd : {X : Type u_1} →
  {Y : Type u_2} →
    {R : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : CommRing R] →
            [inst_3 : TopologicalSpace R] →
              [inst_4 : IsTopologicalRing R] → AbstractMeasure Y R R →ₗ[R] C(X × Y, R) →ₗ[R] C(X, R)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance!_eq_balanceₘ : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size ∨
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size →
        Std.DTreeMap.Internal.Impl.balance! k v l r = Std.DTreeMap.Internal.Impl.balanceₘ k v l r
-- Mathlib.RingTheory.Bialgebra.TensorProduct
/-- The associator for tensor products of R-bialgebras, as a bialgebra equivalence.  -/
Bialgebra.TensorProduct.assoc : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      (C : Type u_5) →
        (D : Type u_6) →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : Semiring A] →
                [inst_3 : Bialgebra S A] →
                  [inst_4 : Algebra R A] →
                    [inst_5 : Algebra R S] →
                      [inst_6 : IsScalarTower R S A] →
                        [inst_7 : Semiring C] →
                          [inst_8 : Semiring D] →
                            [inst_9 : Bialgebra S C] →
                              [inst_10 : Bialgebra R D] →
                                [inst_11 : Algebra R C] →
                                  [inst_12 : IsScalarTower R S C] →
                                    TensorProduct R (TensorProduct S A C) D ≃ₐc[S]
                                      TensorProduct S A (TensorProduct R C D)
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_add_fract_le : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a b : R),
  Int.fract a + Int.fract b ≤ Int.fract (a + b) + 1
-- Mathlib.Algebra.Group.Defs
add_sub_cancel_right : ∀ {G : Type u_1} [inst : AddGroup G] (a b : G), a + b - b = a
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.of.injEq : ∀ {C : Type u} (a a_1 : C), (CategoryTheory.WithTerminal.of a = CategoryTheory.WithTerminal.of a_1) = (a = a_1)
-- Mathlib.Analysis.Real.Hyperreal
/-- Natural embedding `ℝ → ℝ*`.  -/
Hyperreal.ofReal : ℝ → ℝ*
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.getKeyD_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, m₁.Equiv m₂ → m₁.getKeyD k fallback = m₂.getKeyD k fallback
-- Mathlib.Data.List.Sigma
List.kextract.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (x : List (Sigma β)),
  List.kextract a x =
    match x with
    | [] => (none, [])
    | s :: l =>
      if h : s.fst = a then (some (Eq.recOn h s.snd), l)
      else
        match List.kextract a l with
        | (b', l') => (b', s :: l')
-- Mathlib.Data.Set.Lattice
Set.iInter_true : ∀ {α : Type u_1} {s : True → Set α}, Set.iInter s = s trivial
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.op_pOpcycles_opcyclesOpIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp S.op.pOpcycles S.opcyclesOpIso.hom = S.iCycles.op
-- Mathlib.RingTheory.Etale.QuasiFinite
/-- If `S` is finite over `R`, and `p` is a prime of `R`, then there exists an étale neighborhood
`(R', P)` of `p` with `κ(p) = κ(P)` such that `R' ⊗[R] S ≃ₐ[R'] R₁ × ... × Rₙ × A`,
each `Rᵢ` has a unique prime `Pᵢ` lying over `P`, and no other prime in `R' ⊗[R] S` lies over `P`.

This is merely an iterated application of `exists_etale_isIdempotentElem_forall_liesOver_eq`.
This is weaker than the corresponding statement of stacks project (in particular we asked for
`Module.Finite` instead of quasi finite when localized at `p`, so that we don't need to keep
track of this when passing to quotients and tensor products), and the only reason is that
the corresponding stronger statement is even harder to state and even more annoying to prove.
 -/
Algebra.exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Finite R S]
  (p : Ideal R) [inst_4 : p.IsPrime],
  ∃ R' x x_1,
    ∃ (_ : Algebra.Etale R R'),
      ∃ P,
        ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
          ∃ n e,
            ∃ (_ : CompleteOrthogonalIdempotents e),
              ∃ P',
                ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                  Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (Algebra.ofId R R') ⋯) ∧
                    (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                      ∀ (P'' : Ideal (TensorProduct R R' S)),
                        P''.IsPrime →
                          P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
-- Mathlib.Tactic.Convert
/-- Configuration for the `convert!` family of tactics.
This is `Convert.CheapConfig` (used by `convert` without exclamation mark) with different,
more aggressive, defaults.

To elaborate config options for `convert`, use `Convert.elabConfig` which chooses
between `Convert.CheapConfig` and `Convert.ExpensiveConfig` based on other flags.

We separate out the two structures to allow the user to explicitly set options in the call, so for
example the following call runs at `.instances` transparency.
```
convert! (postTransparency := .instances)
```
 -/
Convert.ExpensiveConfig : Type
-- Init.Prelude
/-- `(panic "msg" : α)` has a built-in implementation which prints `msg` to
the error buffer. It *does not* terminate execution, and because it is a safe
function, it still has to return an element of `α`, so it takes `[Inhabited α]`
and returns `default`. It is primarily intended for debugging in pure contexts,
and assertion failures.

Because this is a pure function with side effects, it is marked as
`@[never_extract]` so that the compiler will not perform common sub-expression
elimination and other optimizations that assume that the expression is pure.
 -/
panic : {α : Sort u} → [Inhabited α] → String → α
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.nl : Lean.Parser.ParserFn
-- Init.Data.Format.Syntax
Lean.Syntax.instToString : ToString Lean.Syntax
-- Init.Control.MonadAttach
MonadAttach.mk : {m : Type u → Type v} →
  (CanReturn : {α : Type u} → m α → α → Prop) → ({α : Type u} → (x : m α) → m (Subtype (CanReturn x))) → MonadAttach m
-- Mathlib.Analysis.Convex.GaugeRescale
gauge_gaugeRescale : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [T1Space E] (s : Set E)
  {t : Set E}, Absorbent ℝ t → Bornology.IsVonNBounded ℝ t → ∀ (x : E), gauge t (gaugeRescale s t x) = gauge s x
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_eq_extractLsb : ∀ {w : ℕ} (x : BitVec w) (start len : ℕ) (h : len > 0),
  BitVec.extractLsb' start len x = BitVec.cast ⋯ (BitVec.extractLsb (len - 1 + start) start x)