mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
right_le_midpoint : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E}, b ≤ midpoint k a b ↔ b ≤ a
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.ιMapBifunctor.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) [inst_5 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] [inst_8 : K₁.HasMapBifunctor K₂ F] (n₁ n₂ n : ℤ)
  (h : n₁ + n₂ = n), K₁.ιMapBifunctor K₂ F n₁ n₂ n h = K₁.ιMapBifunctor K₂ F n₁ n₂ n h
-- Mathlib.Algebra.Group.Hom.Defs
OneHomClass.toOneHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
  [inst_3 : OneHomClass F M N] (f : F), ↑f = { toFun := ⇑f, map_one' := ⋯ }
-- Lean.Meta.PPGoal
Lean.Meta.pp.showLetValues.threshold : Lean.Option ℕ
-- Mathlib.Algebra.CharP.Algebra
/-- If `R` has characteristic `0`, then so does Frac(R).  -/
IsFractionRing.charZero_of_isFractionRing : ∀ (R : Type u_3) {K : Type u_4} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [CharZero R], CharZero K
-- Lean.Elab.PreDefinition.WF.Unfold
_private.Lean.Elab.PreDefinition.WF.Unfold.0.Lean.Elab.WF.rwFixEq : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Init.Data.Nat.Lemmas
/-- Tail-recursive `Bool` loop: `true` iff `f i h` holds for some `i < n`
(short-circuits on the first `true`). Used at runtime by `decidableExistsLT`/`'` via `@[csimp]`.  -/
Nat.anyLTTR : (n : ℕ) → ((i : ℕ) → i < n → Bool) → Bool
-- Mathlib.Algebra.Order.Archimedean.Basic
instArchimedeanRat : Archimedean ℚ
-- Mathlib.Data.Analysis.Topology
/-- A `Ctop` realizer for the topological space `T` is a `Ctop`
which generates `T`.  -/
Ctop.Realizer : (α : Type u_6) → [T : TopologicalSpace α] → Type (max (u_5 + 1) u_6)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepSets_of_indepSets_of_le_right : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ s₂ s₃ : Set (Set Ω)},
  ProbabilityTheory.IndepSets s₁ s₂ μ → s₃ ⊆ s₂ → ProbabilityTheory.IndepSets s₁ s₃ μ
-- Mathlib.Algebra.Group.Prod
Prod.commMagma : {M : Type u_3} → {N : Type u_4} → [CommMagma M] → [CommMagma N] → CommMagma (M × N)
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.groupPowers.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {x : M} {n : ℕ} (hpos : 0 < n) (hx : x ^ n = 1),
  Submonoid.groupPowers hpos hx =
    { toMonoid := (Submonoid.powers x).toMonoid, inv := fun x_1 => x_1 ^ (n - 1), div := DivInvMonoid.div',
      zpow := fun z x_1 => x_1 ^ z.natMod ↑n, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯,
      inv_mul_cancel := ⋯ }
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- If two continuous linear maps are equal on a set `s`, then they are equal on the closure
of the `Submodule.span` of this set.  -/
ContinuousLinearMap.eqOn_closure_span : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [T2Space M₂] {s : Set M₁}
  {f g : M₁ →SL[σ₁₂] M₂}, Set.EqOn (⇑f) (⇑g) s → Set.EqOn (⇑f) (⇑g) (closure ↑(Submodule.span R₁ s))
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.addLeft.eq_1 : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : SeparatelyContinuousAdd G] (a : G),
  Homeomorph.addLeft a = { toEquiv := Equiv.addLeft a, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Data.Finset.Functor
Finset.map_comp_coe_apply : ∀ {α β : Type u} (h : α → β) (s : Multiset α), Finset.image h s.toFinset = (h <$> s).toFinset
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.pow_ne_one_of_pos_of_lt : ∀ {M : Type u_1} [inst : CommMonoid M] {k l : ℕ} {ζ : M}, IsPrimitiveRoot ζ k → l ≠ 0 → l < k → ζ ^ l ≠ 1
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.jacobian_isUnit : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Finite σ] (self : Algebra.SubmersivePresentation R S ι σ), IsUnit self.jacobian
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.insertMany_append : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {l₁ l₂ : List α},
  t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.symm_mk : ∀ {V : Type u_1} {G : SimpleGraph V} {p : V × V} (h : G.Adj p.1 p.2),
  { toProd := p, adj := h }.symm = { toProd := p.swap, adj := ⋯ }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        ∀ {v : β},
          List.Pairwise (fun a b => (a.1 == b.1) = false) l →
            (k, v) ∈ l →
              ∀ {h' : (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).contains k' = true},
                Std.DHashMap.Internal.Raw₀.Const.get (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k' h' = v
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_inv_ofNat_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : StarAddMonoid α] [inst_3 : Module R α] (c : ℕ) [inst_4 : c.AtLeastTwo] (M : Matrix m n α),
  ((OfNat.ofNat c)⁻¹ • M).conjTranspose = (OfNat.ofNat c)⁻¹ • M.conjTranspose
-- Mathlib.LinearAlgebra.PiTensorProduct.Basis
Basis.piTensorProduct_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} {κ : ι → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Finite ι]
  (b : (i : ι) → Module.Basis (κ i) R (M i)) (p : (i : ι) → κ i),
  (Basis.piTensorProduct b) p = ⨂ₜ[R] (i : ι), (b i) (p i)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.congr_fun : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {f g : X →ₑ[φ] Y}, f = g → ∀ (x : X), f x = g x
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_le_pow_right₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} {m n : ℕ} [ZeroLEOneClass M₀]
  [PosMulMono M₀], 1 ≤ a → m ≤ n → a ^ m ≤ a ^ n
-- Mathlib.Order.Partition.Basic
Partition.mk.inj : ∀ {α : Type u_1} {inst : CompleteLattice α} {s : α} {parts : Set α} {sSupIndep' : sSupIndep parts}
  {bot_notMem' : ⊥ ∉ parts} {sSup_eq' : sSup parts = s} {parts_1 : Set α} {sSupIndep'_1 : sSupIndep parts_1}
  {bot_notMem'_1 : ⊥ ∉ parts_1} {sSup_eq'_1 : sSup parts_1 = s},
  { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' } =
      { parts := parts_1, sSupIndep' := sSupIndep'_1, bot_notMem' := bot_notMem'_1, sSup_eq' := sSup_eq'_1 } →
    parts = parts_1
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
/-- Given a directed system of `R`-modules, tensoring it on the right gives a directed system  -/
DirectedSystem.rTensor : ∀ (R : Type u) (N : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N] {ι : Type u_3}
  [inst_3 : Preorder ι] {F : ι → Type u_4} [inst_4 : (i : ι) → AddCommMonoid (F i)] [inst_5 : (i : ι) → Module R (F i)]
  {f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j},
  (DirectedSystem F fun x x_1 h => ⇑(f h)) →
    DirectedSystem (fun i => TensorProduct R (F i) N) fun x x_1 h => ⇑(LinearMap.rTensor N (f h))