mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.H1Cotangent.map_comp_apply : ∀ {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'} {S' : Type v'} [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'] {R'' : Type u''} {S'' : Type v''} [inst_10 : CommRing R''] [inst_11 : CommRing S'']
  [inst_12 : Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [inst_13 : Algebra R R''] [inst_14 : Algebra S S'']
  [inst_15 : Algebra R S''] [inst_16 : IsScalarTower R R'' S''] [inst_17 : Algebra R' R''] [inst_18 : Algebra S' S'']
  [inst_19 : Algebra R' S''] [inst_20 : IsScalarTower R' R'' S''] [inst_21 : IsScalarTower R R' R'']
  [inst_22 : IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') (x : P.H1Cotangent),
  (Algebra.Extension.H1Cotangent.map (g.comp f)) x =
    (Algebra.Extension.H1Cotangent.map g) ((Algebra.Extension.H1Cotangent.map f) x)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get?_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∩ t₂).get? k = none
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mk.injEq : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (toSubalgebra : Subalgebra K L) (inv_mem' : ∀ x ∈ toSubalgebra.carrier, x⁻¹ ∈ toSubalgebra.carrier)
  (toSubalgebra_1 : Subalgebra K L) (inv_mem'_1 : ∀ x ∈ toSubalgebra_1.carrier, x⁻¹ ∈ toSubalgebra_1.carrier),
  ({ toSubalgebra := toSubalgebra, inv_mem' := inv_mem' } =
      { toSubalgebra := toSubalgebra_1, inv_mem' := inv_mem'_1 }) =
    (toSubalgebra = toSubalgebra_1)
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.iterate.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.MetricSpace.Ultra.TotallySeparated
instTotallySeparatedSpaceOfIsUltrametricDist : ∀ {X : Type u_1} [inst : MetricSpace X] [IsUltrametricDist X], TotallySeparatedSpace X
-- Mathlib.ModelTheory.Order
FirstOrder.Language.Term.realize_le : ∀ {L : FirstOrder.Language} {α : Type w} {M : Type w'} {n : ℕ} [inst : L.IsOrdered] [inst_1 : L.Structure M]
  [inst_2 : LE M] [L.OrderedStructure M] {t₁ t₂ : L.Term (α ⊕ Fin n)} {v : α → M} {xs : Fin n → M},
  (t₁.le t₂).Realize v xs ↔
    FirstOrder.Language.Term.realize (Sum.elim v xs) t₁ ≤ FirstOrder.Language.Term.realize (Sum.elim v xs) t₂
-- Init.Data.Array.Lemmas
Array.reverse_eq_append_iff : ∀ {α : Type u_1} {xs ys zs : Array α}, xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieModule.IsTriangularizable R L M], LieModule.IsTriangularizable R (↥(LieModule.toEnd R L M).range) M
-- Lean.Expr
Lean.ExprStructEq.instBEq : BEq Lean.ExprStructEq
-- Mathlib.LinearAlgebra.TensorProduct.Opposite
Algebra.TensorProduct.opAlgEquiv_tmul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] (a : Aᵐᵒᵖ) (b : Bᵐᵒᵖ),
  (Algebra.TensorProduct.opAlgEquiv R S A B) (a ⊗ₜ[R] b) = MulOpposite.op (MulOpposite.unop a ⊗ₜ[R] MulOpposite.unop b)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_union : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t₁ t₂ : Finset β}
  [inst_2 : DecidableEq β], s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂)
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.HasInjectiveDimensionLT.subsingleton : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) (n : ℕ) [hX : CategoryTheory.HasInjectiveDimensionLT X n] (i : ℕ),
  n ≤ i → ∀ (Y : C), Subsingleton (CategoryTheory.Abelian.Ext Y X i)
-- Mathlib.Algebra.Lie.Graded
LieDerivation.ofGrading_apply_apply : ∀ {ι : Type u_1} {R : Type u_3} {L : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid ι] [inst_2 : CommRing R]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ℒ : ι → Submodule R L) [inst_5 : GradedLieAlgebra ℒ] (φ : ι →+ R)
  {i : ι} {a : L}, a ∈ ℒ i → (LieDerivation.ofGrading ℒ φ) a = φ i • a
-- Mathlib.Data.Set.Function
Set.injOn_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ {s : Set α}, Set.InjOn f s
-- Mathlib.NumberTheory.NumberField.FractionalIdeal
NumberField.basisOfFractionalIdeal_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) (i : Module.Free.ChooseBasisIndex ℤ ↥↑↑I),
  (NumberField.basisOfFractionalIdeal K I) i = ↑((NumberField.fractionalIdealBasis K ↑I) i)
-- Mathlib.Topology.Compactness.SigmaCompact
/-- If `X` is σ-compact, `im f` is σ-compact.  -/
isSigmaCompact_range : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ [SigmaCompactSpace X], IsSigmaCompact (Set.range f)
-- Lean.Parser.Command
Lean.Parser.Command.meta.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.MethodSpecsSimp
Mod.mod_eq_hMod : ∀ {α : Type u_1} [inst : Mod α], Mod.mod = HMod.hMod
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
Differentiable.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {H : Type u_5}
  [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G},
  Differentiable 𝕜 c → Differentiable 𝕜 u → Differentiable 𝕜 fun y => (c y) (u y)
-- Init.Data.Range.Polymorphic.NatLemmas
Array.range_eq_toArray_rco : ∀ {n : ℕ}, Array.range n = (0...n).toArray
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α},
  m.size ≤ (m.insertManyIfNewUnit l).size
-- Mathlib.Tactic.GCongr.Core
/-- The name of the head function. For example, `a + b ≤ a + c` has ``head := `HAdd.hAdd``.  -/
Mathlib.Tactic.GCongr.GCongrKey.head : Mathlib.Tactic.GCongr.GCongrKey → Lean.Name
-- Mathlib.Analysis.ODE.PicardLindelof
/-- `L` is an upper bound of the norm of the vector field.  -/
IsPicardLindelof.norm_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E}
  {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K → ∀ t ∈ Set.Icc tmin tmax, ∀ x ∈ Metric.closedBall x₀ ↑a, ‖f t x‖ ≤ ↑L
-- Mathlib.Topology.Specialization
Specialization.toEquiv_le_toEquiv : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a b : α}, Specialization.toEquiv a ≤ Specialization.toEquiv b ↔ b ⤳ a
-- Mathlib.Algebra.Group.End
/-- The group of multiplicative automorphisms.  -/
MulAut : (M : Type u_7) → [Mul M] → Type u_7
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
/-- If `L` is a localization functor for `W` and `e : F ≅ L ⋙ G` is an isomorphism,
then `e.hom` makes `G` a pointwise left Kan extension of `F` along `L`.  -/
CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsoOfIsLocalization : {C : Type u₁} →
  {D : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            {F : CategoryTheory.Functor C H} →
              {L : CategoryTheory.Functor C D} →
                (W : CategoryTheory.MorphismProperty C) →
                  {G : CategoryTheory.Functor D H} →
                    (e : F ≅ L.comp G) →
                      [L.IsLocalization W] →
                        (CategoryTheory.Functor.LeftExtension.mk G e.hom).IsPointwiseLeftKanExtension
-- Mathlib.RingTheory.ZariskisMainTheorem
/-- The algebraic version of **Zariski's Main Theorem**:
Given a finite type `R`-algebra `S` that is quasi-finite at a prime `p`,
there exists a `f ∉ p` such that `S[1/f]` is isomorphic to `R'[1/f]` where `R'` is the integral
closure of `R` in `S`.
 -/
Algebra.ZariskisMainProperty.of_finiteType : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Algebra.FiniteType R S]
  (p : Ideal S) [inst_4 : p.IsPrime] [Algebra.QuasiFiniteAt R p], Algebra.ZariskisMainProperty R p
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.below.mul : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop}
  {motive : (a a_1 : R) → RingConGen.Rel r a a_1 → Prop} {w x y z : R} (a : RingConGen.Rel r w x)
  (a_1 : RingConGen.Rel r y z),
  RingConGen.Rel.below a → motive w x a → RingConGen.Rel.below a_1 → motive y z a_1 → RingConGen.Rel.below ⋯
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.any_eq_false_iff_forall_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {p : α → Bool},
  m.WF → (m.any p = false ↔ ∀ a ∈ m, p a = false)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.tryRecv' : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadLiftT (ST IO.RealWorld) m] → [MonadLiftT BaseIO m] → ℕ → Std.AtomicT (Std.Bounded.State✝ α) m (Option α)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (Std.ExtDHashMap.ofList l).getKey! k' = k
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.isUnit_det : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e e' : Module.Basis ι R M), IsUnit (e.det ⇑e')
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Equiv.inter_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ m₄ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₃).WF → (↑m₄).WF → (↑m₁).Equiv ↑m₃ → (↑m₂).Equiv ↑m₄ → (↑(m₁.inter m₂)).Equiv ↑(m₃.inter m₄)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instVAdd.eq_1 : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : VAdd R M] [inst_3 : ContinuousConstVAdd R M],
  ContinuousMap.instVAdd = { vadd := fun r f => { toFun := r +ᵥ ⇑f, continuous_toFun := ⋯ } }
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.containsThenInsert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (a : α) (b : β a) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨{ size := size, buckets := buckets }, hm⟩ a b =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ =>
      let bkt := buckets[i];
      if Std.DHashMap.Internal.AssocList.contains a bkt = true then
        let buckets' := buckets.uset i Std.DHashMap.Internal.AssocList.nil h;
        (true, ⟨{ size := size, buckets := buckets'.uset i (Std.DHashMap.Internal.AssocList.replace a b bkt) ⋯ }, ⋯⟩)
      else
        have size' := size + 1;
        let buckets' := buckets.uset i (Std.DHashMap.Internal.AssocList.cons a b bkt) h;
        (false, Std.DHashMap.Internal.Raw₀.expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_prod_left : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'}
  {l : Filter α}, (fun x => (f' x, g' x)) =o[l] k' ↔ f' =o[l] k' ∧ g' =o[l] k'
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsPreBrownianReal.integrable_eval : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P → ∀ (t : NNReal), MeasureTheory.Integrable (B t) P
-- Mathlib.Tactic.NormNum.NatFactorial
/-- Evaluates the Nat.ascFactorial function.  -/
Mathlib.Meta.NormNum.evalNatAscFactorial : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instCanLift : ∀ {α : Type u}, CanLift (WithZero α) α WithZero.coe fun a => a ≠ 0
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.toEquiv_injective : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H},
  Function.Injective AddConstEquiv.toEquiv
-- Init.Data.Nat.Lemmas
Nat.div_eq_sub_mod_div : ∀ {m n : ℕ}, m / n = (m - m % n) / n