mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_update_zero : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι),
  f (Function.update m i 0) = 0
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.strictMonoOn_artanh : StrictMonoOn Real.artanh (Set.Ioo (-1) 1)
-- Init.Data.Float.Float32
/-- Adds two 32-bit floating-point numbers according to IEEE 754. Typically used via the `+` operator.

This function has a logical model in terms of `Float32.Model`. It is compiled to the C addition operator.
 -/
Float32.add : Float32 → Float32 → Float32
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    ∀ (h : Std.Internal.List.containsKey k' (Std.Internal.List.modifyKey k f l) = true),
      Std.Internal.List.getValueCast k' (Std.Internal.List.modifyKey k f l) h =
        if heq : (k == k') = true then cast ⋯ (f (Std.Internal.List.getValueCast k l ⋯))
        else Std.Internal.List.getValueCast k' l ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_eq_getLastD_keys : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l →
      ∀ {fallback : α}, Std.Internal.List.maxKeyD l fallback = (Std.Internal.List.keys l).getLastD fallback
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.map.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f f_1 : P.Hom P'),
  f = f_1 → Algebra.Extension.Cotangent.map f = Algebra.Extension.Cotangent.map f_1
-- Mathlib.Order.Category.BddLat
BddLat.Hom.ext : ∀ {X Y : BddLat} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Mathlib.Algebra.DirectSum.Internal
SetLike.GradeZero.coe_natCast : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : Semiring R] [inst_1 : AddMonoid ι] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : SetLike.GradedMonoid A] (n : ℕ), ↑↑n = ↑n
-- Init.Data.List.Lemmas
List.filter_flatMap : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {g : α → List β} {f : β → Bool},
  List.filter f (List.flatMap g l) = List.flatMap (fun a => List.filter f (g a)) l
-- Mathlib.Combinatorics.SimpleGraph.Hall
/-- Given a partition `p` and a function `f` mapping vertices in `p` to the other partition, create
the subgraph including only the edges between `x` and `f x` for all `x` in `p`.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Hall.0.SimpleGraph.hall_subgraph : {V : Type u_1} →
  {G : SimpleGraph V} →
    {p : Set V} →
      [DecidablePred fun x => x ∈ p] →
        (f : ↑p → V) → (∀ (x : ↑p), f x ∉ p) → (∀ (x : ↑p), G.Adj (↑x) (f x)) → G.Subgraph
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit.injEq : ∀ {α : Type u} (l l_1 : Std.Sat.Literal α),
  (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l =
      Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l_1) =
    (l = l_1)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractRight_mul_algebraMap : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (d : Module.Dual R M) (a : CliffordAlgebra Q) (r : R),
  (CliffordAlgebra.contractRight (a * (algebraMap R (CliffordAlgebra Q)) r)) d =
    (CliffordAlgebra.contractRight a) d * (algebraMap R (CliffordAlgebra Q)) r
-- Mathlib.Order.Heyting.Basic
Pi.instGeneralizedCoheytingAlgebra : {ι : Type u_1} →
  {α : ι → Type u_4} → [(i : ι) → GeneralizedCoheytingAlgebra (α i)] → GeneralizedCoheytingAlgebra ((i : ι) → α i)
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.below.of : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} {motive : (a a_1 : R) → RingQuot.Rel r a a_1 → Prop} ⦃x y : R⦄
  (h : r x y), RingQuot.Rel.below ⋯
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.matched.inj : ∀ {s : String.Slice} {startPos endPos startPos_1 endPos_1 : s.Pos},
  String.Slice.Pattern.SearchStep.matched startPos endPos =
      String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1 →
    startPos = startPos_1 ∧ endPos = endPos_1
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.instCoeOutLinearEquivId : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {B₁ : LinearMap.BilinForm R M₁} →
                  {B₂ : LinearMap.BilinForm R M₂} → CoeOut (B₁.IsometryEquiv B₂) (M₁ ≃ₗ[R] M₂)
-- Mathlib.Topology.Path
Path.truncate_range : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) {t₀ t₁ : ℝ},
  Set.range ⇑(γ.truncate t₀ t₁) ⊆ Set.range ⇑γ
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.eqLocus.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddMonoid M] (f g : G →+ M),
  f.eqLocus g = { toAddSubmonoid := f.eqLocusM g, neg_mem' := ⋯ }
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.Cat.closed : (C : Type u) → [inst : CategoryTheory.Category.{u, u} C] → CategoryTheory.Closed (CategoryTheory.Cat.of C)
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- A variant of `IsAdicComplete.lift`. Only takes `f n : M →ₗ[R] N ⧸ (I ^ (a n) • ⊤)`
from a strictly increasing sequence `a n`.
 -/
IsAdicComplete.StrictMono.lift : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {M : Type u_4} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type u_5} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {a : ℕ → ℕ} →
                    (ha : StrictMono a) →
                      (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) →
                        (∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) → [IsAdicComplete I N] → M →ₗ[R] N
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The morphism `X ⟶ Y` corresponding to a morphism `𝟙_ C ⟶ (ihom X).obj Y`.  -/
CategoryTheory.MonoidalClosed.uncurry' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : C} →
        [inst_2 : CategoryTheory.Closed X] → (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X ⟹ Y) → (X ⟶ Y)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.neg : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E],
  ProbabilityTheory.HasGaussianLaw X P → ProbabilityTheory.HasGaussianLaw (-X) P
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The unit associated to a representative of `P + Q` for two Jacobian point representatives `P`
and `Q` on a Weierstrass curve `W` that are not `2`-torsion.

More specifically, the unit `u` such that `W.add P Q = u • ![1, 1, 0]` where
`P x / P z ^ 2 = Q x / Q z ^ 2` but `P ≠ W.neg P`.  -/
WeierstrassCurve.Jacobian.addU : {F : Type u} → [Field F] → (Fin 3 → F) → (Fin 3 → F) → F
-- Lean.Elab.Do.Basic
/-- The `FVarId` of the initial binding produced by `let mut`.  -/
Lean.Elab.Do.MutVar.baseId : Lean.Elab.Do.MutVar → Lean.FVarId
-- Mathlib.Logic.Basic
congr_refl_right : ∀ {α : Sort u_1} {β : Sort u_2} {f g : α → β} (h : f = g) (a : α), ⋯ = ⋯
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.prod_source : ∀ {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Y']
  (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y'), (eX.prod eY).source = eX.source ×ˢ eY.source
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil.Sorted
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsPreLocalizingSequence.congr_simp : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : Preorder ι] [inst_1 : TopologicalSpace ι]
  [inst_2 : OrderTopology ι] (𝓕 𝓕_1 : MeasureTheory.Filtration ι mΩ),
  𝓕 = 𝓕_1 →
    ∀ (τ τ_1 : ℕ → Ω → WithTop ι),
      τ = τ_1 →
        ∀ (P P_1 : MeasureTheory.Measure Ω),
          P = P_1 →
            ProbabilityTheory.IsPreLocalizingSequence 𝓕 τ P = ProbabilityTheory.IsPreLocalizingSequence 𝓕_1 τ_1 P_1
-- Mathlib.MeasureTheory.Measure.Real
/-- If two sets are equal modulo a set of measure zero, then `μ.real s = μ.real t`.  -/
MeasureTheory.measureReal_congr : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, s =ᵐ[μ] t → μ.real s = μ.real t
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : NonAssocSemiring α] →
      [inst_1 : Preorder α] →
        [inst_2 : NonAssocSemiring β] →
          [inst_3 : Preorder β] → (toRingHom : α →+* β) → Monotone (↑↑toRingHom).toFun → α →+*o β
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.Box.measure_Icc_lt_top : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsLocallyFiniteMeasure μ],
  μ (BoxIntegral.Box.Icc I) < ⊤
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instInfSet : (M : Type u_1) → [inst : AddZeroClass M] → InfSet (SaturatedAddSubmonoid M)
-- Init.Data.List.Basic
List.erase.eq_def : ∀ {α : Type u_1} [inst : BEq α] (x : List α) (x_1 : α),
  x.erase x_1 =
    match x, x_1 with
    | [], x => []
    | a :: as, b =>
      match a == b with
      | true => as
      | false => a :: as.erase b
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
/-- If `φ : a ⟶ b` lifts `𝟙 T` and `ψ : b ⟶ c` lifts `f`, then `φ  ≫ ψ` lifts `f`  -/
CategoryTheory.IsHomLift.comp_lift_id_left' : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {a b c : 𝒳} (R : 𝒮) (φ : a ⟶ b) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) φ]
  {S T : 𝒮} (f : S ⟶ T) (ψ : b ⟶ c) [p.IsHomLift f ψ], p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ ψ)
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Show that `G` preserves left Kan extensions if it maps some left Kan extension to a left
Kan extension.  -/
CategoryTheory.Functor.PreservesLeftKanExtension.mk_of_preserves_isLeftKanExtension : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) (F' : CategoryTheory.Functor C B) (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α],
  (F'.comp G).IsLeftKanExtension
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α G) (L.associator F' G).hom) →
    G.PreservesLeftKanExtension F L
-- Mathlib.RingTheory.Adjoin.Field
minpoly_add_algebraMap_splits : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L} (r : K),
  (Polynomial.map (algebraMap K L) (minpoly K x)).Splits →
    (Polynomial.map (algebraMap K L) (minpoly K (x + (algebraMap K L) r))).Splits
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.instIsScalarTower : ∀ {M : Type u_1} {N : Type u_2} {R : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] [inst_4 : MulSemiringAction N R] [inst_5 : SMul M N] [IsScalarTower M N R],
  IsScalarTower M N (Ideal R)
-- Std.Internal.Do.Order.Basic
/-- Entailment between functions follows from pointwise entailment.  -/
Lean.Order.le_of_forall_le : ∀ {σ α : Type u} [inst : Lean.Order.PartialOrder α] {f g : σ → α},
  (∀ (s : σ), Lean.Order.PartialOrder.rel (f s) (g s)) → Lean.Order.PartialOrder.rel f g
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndinter_subset_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s.ndinter t ⊆ s
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_eq_none : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a : α}, a ∉ m → m.get? a = none
-- Mathlib.Control.Fold
/-- For a list, foldl f x [y₀,y₁] reduces as follows:

```
calc  foldl f x [y₀,y₁]
    = foldl f (f x y₀) [y₁]      : rfl
... = foldl f (f (f x y₀) y₁) [] : rfl
... = f (f x y₀) y₁              : rfl
```
with
```
f : α → β → α
x : α
[y₀,y₁] : List β
```

We can view the above as a composition of functions:
```
... = f (f x y₀) y₁              : rfl
... = flip f y₁ (flip f y₀ x)    : rfl
... = (flip f y₁ ∘ flip f y₀) x  : rfl
```

We can use traverse and const to construct this composition:
```
calc   const.run (traverse (fun y ↦ const.mk' (flip f y)) [y₀,y₁]) x
     = const.run ((::) <$> const.mk' (flip f y₀) <*>
         traverse (fun y ↦ const.mk' (flip f y)) [y₁]) x
...  = const.run ((::) <$> const.mk' (flip f y₀) <*>
         ( (::) <$> const.mk' (flip f y₁) <*> traverse (fun y ↦ const.mk' (flip f y)) [] )) x
...  = const.run ((::) <$> const.mk' (flip f y₀) <*>
         ( (::) <$> const.mk' (flip f y₁) <*> pure [] )) x
...  = const.run ( ((::) <$> const.mk' (flip f y₁) <*> pure []) ∘
         ((::) <$> const.mk' (flip f y₀)) ) x
...  = const.run ( const.mk' (flip f y₁) ∘ const.mk' (flip f y₀) ) x
...  = const.run ( flip f y₁ ∘ flip f y₀ ) x
...  = f (f x y₀) y₁
```

And this is how `const` turns a monoid into an applicative functor and
how the monoid of endofunctions define `Foldl`.
 -/
Monoid.Foldl : Type u → Type u
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.weakFEPair.eq_1 : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : ModularFormClass F Γ k],
  ModularForm.weakFEPair hk f =
    { f := fun t => f (↑UpperHalfPlane.ofComplex (Complex.I * ↑t)),
      g := fun t =>
        (ModularForm.translate f
            (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))
          (↑UpperHalfPlane.ofComplex (Complex.I * ↑t)),
      k := ↑k, ε := Complex.I ^ k, f₀ := UpperHalfPlane.valueAtInfty ⇑f,
      g₀ :=
        UpperHalfPlane.valueAtInfty
          ⇑(ModularForm.translate f
              (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))),
      hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }
-- Mathlib.MeasureTheory.Measure.OpenPos
/-- See also `Metric.measure_closedBall_pos_iff`.  -/
Metric.measure_closedBall_pos : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  (x : X) {r : ℝ}, 0 < r → 0 < μ (Metric.closedBall x r)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
Std.IterM.dropWhileWithPostcondition_eq_intermediateDropWhileWithPostcondition : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Std.Iterator α m β] {it : Std.IterM m β}
  {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)},
  Std.IterM.dropWhileWithPostcondition P it = Std.IterM.Intermediate.dropWhileWithPostcondition P true it
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Prod.pseudoMetricSpaceMax : {α : Type u_1} → {β : Type u_2} → [PseudoMetricSpace α] → [PseudoMetricSpace β] → PseudoMetricSpace (α × β)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toArray_zip_of_finite_right : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂] {it₁ : Std.Iter β₁}
  {it₂ : Std.Iter β₂} [Std.Iterators.Productive α₁ Id] [Std.Iterators.Finite α₂ Id],
  (it₁.zip it₂).toArray = (Std.Iter.take it₂.toArray.size it₁).toArray.zip it₂.toArray
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.integral_deriv_eq_sub' : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f' : ℝ → E}
  (f : ℝ → E),
  deriv f = f' →
    (∀ x ∈ Set.uIcc a b, DifferentiableAt ℝ f x) → ContinuousOn f' (Set.uIcc a b) → ∫ (y : ℝ) in a..b, f' y = f b - f a
-- Mathlib.RingTheory.Adjoin.PowerBasis
/-- Let `B B' : PowerBasis K S` be such that `IsIntegral R B.gen`, and let `P : R[X]` be such that
`aeval B.gen P = B'.gen`. Then `IsIntegral R (B.basis.to_matrix B'.basis i j)` for all `i` and `j`
if `minpoly K B.gen = (minpoly R B.gen).map (algebraMap R L)`. This is the case
if `R` is a GCD domain and `K` is its fraction ring.  -/
PowerBasis.toMatrix_isIntegral : ∀ {K : Type u_1} {S : Type u_2} [inst : Field K] [inst_1 : CommRing S] [inst_2 : Algebra K S] {R : Type u_3}
  [inst_3 : CommRing R] [inst_4 : Algebra R S] [inst_5 : Algebra R K] [IsScalarTower R K S] {B B' : PowerBasis K S}
  {P : Polynomial R},
  (Polynomial.aeval B.gen) P = B'.gen →
    IsIntegral R B.gen →
      minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen) →
        ∀ (i : Fin B.dim) (j : Fin B'.dim), IsIntegral R (B.basis.toMatrix (⇑B'.basis) i j)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.S.instEpiSimplexCategoryToNπ : ∀ {X : SSet} (x : X.S), CategoryTheory.Epi x.toNπ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false → (Std.TreeMap.ofList l cmp).getKeyD k fallback = fallback
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.MeasureSpace.pi : {ι : Type u_1} →
  [Fintype ι] →
    {α : ι → Type u_4} → [(i : ι) → MeasureTheory.MeasureSpace (α i)] → MeasureTheory.MeasureSpace ((i : ι) → α i)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_tsub_tsub_cancel_left : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable (a - b) → b ≤ a → a - c - (a - b) = b - c
-- Init.Data.Int.LemmasAux
Int.pos_iff_toNat_pos : ∀ {n : ℤ}, 0 < n ↔ 0 < n.toNat
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.State.nextIdx : Lean.Meta.SynthInstance.MkTableKey.State → ℕ
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.add_const_right : ∀ {w a : ℕ} {b : BitVec w} {c : ℕ}, BitVec.ofNat w a + (b + BitVec.ofNat w c) = BitVec.ofNat w a + BitVec.ofNat w c + b
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.exists_eq_mk₂ : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] (z w : DirectLimit F f),
  ∃ i x y, z = ⟦⟨i, x⟩⟧ ∧ w = ⟦⟨i, y⟩⟧
-- Mathlib.Data.Finset.Image
Finset.image_inter_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] (f : α → β) (s t : Finset α),
  Finset.image f (s ∩ t) ⊆ Finset.image f s ∩ Finset.image f t
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.exist_unique_vadd_mem_fundamentalDomain : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [IsStrictOrderedRing K] [FloorRing K]
  [Finite ι] (x : E), ∃! v, v +ᵥ x ∈ ZSpan.fundamentalDomain b
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.TransversalPair.mk.sizeOf_spec : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} [inst_1 : SizeOf G] (set : ℤˣ → Set G)
  (compl : ∀ (u : ℤˣ), Subgroup.IsComplement (↑(HNNExtension.toSubgroup A B u)) (set u)),
  sizeOf { set := set, compl := compl } = 1
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a `G`-representation `A` and a normal subgroup `S ≤ G`, the short complex
`H¹(G ⧸ S, A^S) ⟶ H¹(G, A) ⟶ H¹(S, A)` is exact.  -/
groupCohomology.H1InfRes_exact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupCohomology.H1InfRes A S).Exact
-- Std.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.Equiv.toList_eq : ∀ {α₁ β α₂ : Type u_1} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [Std.Iterators.Finite α₁ Id]
  [Std.Iterators.Finite α₂ Id] {ita : Std.Iter β} {itb : Std.Iter β}, ita.Equiv itb → ita.toList = itb.toList
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn_ι_assoc : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn f c)
      (CategoryTheory.CategoryStruct.comp (f.filtration j).ι h) =
    CategoryTheory.CategoryStruct.comp c.horn.ι (CategoryTheory.CategoryStruct.comp c.map h)
-- Mathlib.Algebra.Group.Action.Prod
/-- Construct a `MulAction` by a product monoid from `MulAction`s by the factors.
This is not an instance to avoid diamonds for example when `α := M × N`.  -/
MulAction.prodOfSMulCommClass : (M : Type u_1) →
  (N : Type u_2) →
    (α : Type u_5) →
      [inst : Monoid M] →
        [inst_1 : Monoid N] →
          [inst_2 : MulAction M α] → [inst_3 : MulAction N α] → [SMulCommClass M N α] → MulAction (M × N) α
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
TopCat.instIsStableUnderBaseChangeIsOpenEmbedding : TopCat.isOpenEmbedding.IsStableUnderBaseChange
-- Mathlib.Analysis.BoundedVariation
/-- A real function into a finite-dimensional real vector space which is Lipschitz on a set
is differentiable almost everywhere in this set. For the general Rademacher theorem assuming
that the source space is finite dimensional, see `LipschitzOnWith.ae_differentiableWithinAt_of_mem`.
 -/
LipschitzOnWith.ae_differentiableWithinAt_of_mem_real : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [FiniteDimensional ℝ V] {C : NNReal}
  {f : ℝ → V} {s : Set ℝ}, LipschitzOnWith C f s → ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
-- Mathlib.RingTheory.Localization.Algebra
/-- The canonical linear map from the kernel of `g` to the kernel of its localization.  -/
RingHom.toKerIsLocalization : {R : Type u_1} →
  (S : Type u_2) →
    {P : Type u_3} →
      (Q : Type u_4) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : CommSemiring P] →
              [inst_3 : CommSemiring Q] →
                {M : Submonoid R} →
                  {T : Submonoid P} →
                    [inst_4 : Algebra R S] →
                      [inst_5 : Algebra P Q] →
                        [inst_6 : IsLocalization M S] →
                          [inst_7 : IsLocalization T Q] →
                            (g : R →+* P) →
                              (hy : M ≤ Submonoid.comap g T) →
                                ↥(RingHom.ker g) →ₗ[R] ↥(RingHom.ker (IsLocalization.map Q g hy))