mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.isIso_rightHomologyMap'_of_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ] (h₁ : S₁.RightHomologyData)
  (h₂ : S₂.RightHomologyData), CategoryTheory.IsIso (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂)
-- Mathlib.LinearAlgebra.FreeModule.Basic
/-- **Alias** of `Module.Free.of_equiv`. -/
Module.Free.of_ringEquiv : ∀ {R : Type u_2} {R' : Type u_3} {M : Type u_4} {M' : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M'] [inst_5 : Module R' M'] {σ : R →+* R'}
  {σ' : R' →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ] (e₂ : M ≃ₛₗ[σ] M') [Module.Free R M],
  Module.Free R' M'
-- Mathlib.Order.SuccPred.Basic
Order.Ioo_pred_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Ioo (Order.pred b) a = Set.Ico b a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_succ_right_eq_append : ∀ {m n : ℕ}, m ≤ n → (m<...=n + 1).toList = (m<...=n).toList ++ [n + 1]
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalMVarId : Lean.Meta.ReduceEval Lean.MVarId
-- Batteries.Data.List.Lemmas
List.countBefore_le_count : ∀ {α : Type u_1} {x : α} {i : ℕ} [inst : BEq α] {xs : List α}, List.countBefore x xs i ≤ List.count x xs
-- Mathlib.Data.Rat.Sqrt
Rat.sqrt_nonneg : ∀ (q : ℚ), 0 ≤ Rat.sqrt q
-- Mathlib.Topology.Category.LightProfinite.AsLimit
LightProfinite.proj_comp_transitionMapLE : ∀ (S : LightProfinite) {n m : ℕ} (h : n ≤ m),
  CategoryTheory.CategoryStruct.comp (S.proj m) (S.diagram.map (Opposite.op (CategoryTheory.homOfLE h))) = S.proj n
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_neg : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ), ↑(-r) = -↑r
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.Subobject.eq_of_le_of_isDetecting : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {𝒢 : CategoryTheory.ObjectProperty C},
  𝒢.IsDetecting →
    ∀ {X : C} (P Q : CategoryTheory.Subobject X),
      P ≤ Q → (∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f) → P = Q
-- Mathlib.Order.Partition.Finpartition
Finpartition.parts_inf : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] {a : α}
  (P Q : Finpartition a), (P ⊓ Q).parts = (Finset.image (fun bc => bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)).erase ⊥
-- Mathlib.Data.Finset.Powerset
Finset.powerset_injective : ∀ {α : Type u_1}, Function.Injective Finset.powerset
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {N : Type u_2} →
        [inst_1 : AddCommMonoid N] → (toAddHom : M →ₙ+ N) → S.IsLocalizationMap toAddHom.toFun → S.LocalizationMap N
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.zero' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (self : CategoryTheory.Triangulated.TStructure C) ⦃X Y : C⦄ (f : X ⟶ Y), self.le 0 X → self.ge 1 Y → f = 0
-- Mathlib.Order.Hom.WithTopBot
WithBot.coe_toDualTopEquiv : ∀ {α : Type u_1} [inst : LE α], ⇑WithBot.toDualTopEquiv = ⇑OrderDual.toDual ∘ ⇑WithBot.ofDual
-- Mathlib.CategoryTheory.Limits.Over
/-- `Under.liftCone` is limiting if the original cone is.  -/
CategoryTheory.Under.isLimitLiftCone : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone F) →
            {X : C} →
              (f : X ⟶ c.pt) →
                CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsLimit (CategoryTheory.Under.liftCone c f)
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_subset : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s t : Set 𝕜},
  s ⊆ t → UniqueDiffWithinAt 𝕜 s x → DifferentiableWithinAt 𝕜 f t x → derivWithin f s x = derivWithin f t x
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToIso_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y = Z),
  CategoryTheory.eqToIso p ≪≫ CategoryTheory.eqToIso q = CategoryTheory.eqToIso ⋯
-- Mathlib.Tactic.FBinop
FBinopElab.SRec.args : FBinopElab.SRec → Array Lean.Expr
-- Init.Data.UInt.Bitwise
Bool.toUSize.eq_1 : ∀ (b : Bool), b.toUSize = if b = true then 1 else 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_modify_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} [inst_1 : Inhabited (β k)] {f : β k → β k},
      (Std.DTreeMap.Internal.Impl.modify k f t).get! k = (Option.map f (t.get? k)).get!
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalenceFunctorMonoidal : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).functor.Monoidal
-- Mathlib.Algebra.Module.Prod
Prod.instModule : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : AddCommMonoid N] → [Module R M] → [Module R N] → Module R (M × N)
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_mul_const_of_integrable : ∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {A : Type u_8}
  [inst_1 : NonUnitalNormedRing A] [inst_2 : NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {f : X → A},
  MeasureTheory.Integrable f μ → ∀ {c : A}, ∫ (x : X), f x * c ∂μ = (∫ (x : X), f x ∂μ) * c
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.Section.exists_add_eq_inl_add_add : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  {S : AddGroupExtension N E G} (σ : S.Section) (g₁ g₂ : G), ∃ n, σ (g₁ + g₂) = S.inl n + σ g₁ + σ g₂
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.HasOrthogonalProjection.mk : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E}, (∀ (v : E), ∃ w ∈ K, v - w ∈ Kᗮ) → K.HasOrthogonalProjection
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {fallback : α} {hc : t.minKeyD fallback ∈ t}, t.getKey (t.minKeyD fallback) hc = t.minKeyD fallback
-- Mathlib.GroupTheory.Coset.Defs
AddSubgroup.quotientEquivOfEq.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (h : s = t),
  AddSubgroup.quotientEquivOfEq h =
    { toFun := Quotient.map' id ⋯, invFun := Quotient.map' id ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Computability.Reduce
/-- a computable bijection  -/
Equiv.Computable : {α : Type u_1} → {β : Type u_2} → [Primcodable α] → [Primcodable β] → α ≃ β → Prop
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.sfiniteSeq_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (n : ℕ), MeasureTheory.sfiniteSeq 0 n = 0
-- Lean.Expr
/-- Similar to `isAppOfArity` but skips `Expr.mdata`.  -/
Lean.Expr.isAppOfArity' : Lean.Expr → Lean.Name → ℕ → Bool
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne.match_1.congr_eq_3 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1)
  (x : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) (h_1 : Unit → motive none)
  (h_2 :
    (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      (nodupkey : ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l]) →
        (nodup : [l].Nodup) → motive (some { clause := [l], nodupkey := nodupkey, nodup := nodup }))
  (h_3 : (val : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some val))
  (val : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n),
  x = some val →
    (∀ (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
        (nodupkey : ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l])
        (nodup : [l].Nodup), val = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False) →
      (match x with
        | none => h_1 ()
        | some { clause := [l], nodupkey := nodupkey, nodup := nodup } => h_2 l nodupkey nodup
        | some val => h_3 val) ≍
        h_3 val
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Rel.of_one : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (i : ι),
  Monoid.CoprodI.Rel M (FreeMonoid.of ⟨i, 1⟩) 1
-- Mathlib.Combinatorics.Hindman
Hindman.FS.singleton : ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M) (i : ℕ), a.get i ∈ Hindman.FS a
-- Aesop.RuleSet
Aesop.LocalRuleSet.mk.injEq : ∀ (toBaseRuleSet : Aesop.BaseRuleSet) (simpTheoremsArray : Array (Lean.Name × Lean.Meta.SimpTheorems))
  (simpTheoremsArrayNonempty : 0 < simpTheoremsArray.size) (simprocsArray : Array (Lean.Name × Lean.Meta.Simprocs))
  (simprocsArrayNonempty : 0 < simprocsArray.size) (localNormSimpRules : Array Aesop.LocalNormSimpRule)
  (toBaseRuleSet_1 : Aesop.BaseRuleSet) (simpTheoremsArray_1 : Array (Lean.Name × Lean.Meta.SimpTheorems))
  (simpTheoremsArrayNonempty_1 : 0 < simpTheoremsArray_1.size)
  (simprocsArray_1 : Array (Lean.Name × Lean.Meta.Simprocs)) (simprocsArrayNonempty_1 : 0 < simprocsArray_1.size)
  (localNormSimpRules_1 : Array Aesop.LocalNormSimpRule),
  ({ toBaseRuleSet := toBaseRuleSet, simpTheoremsArray := simpTheoremsArray,
        simpTheoremsArrayNonempty := simpTheoremsArrayNonempty, simprocsArray := simprocsArray,
        simprocsArrayNonempty := simprocsArrayNonempty, localNormSimpRules := localNormSimpRules } =
      { toBaseRuleSet := toBaseRuleSet_1, simpTheoremsArray := simpTheoremsArray_1,
        simpTheoremsArrayNonempty := simpTheoremsArrayNonempty_1, simprocsArray := simprocsArray_1,
        simprocsArrayNonempty := simprocsArrayNonempty_1, localNormSimpRules := localNormSimpRules_1 }) =
    (toBaseRuleSet = toBaseRuleSet_1 ∧
      simpTheoremsArray = simpTheoremsArray_1 ∧
        simprocsArray = simprocsArray_1 ∧ localNormSimpRules = localNormSimpRules_1)
-- Batteries.Lean.AttributeExtra
/-- Registers a new tag attribute. The `extra` field is a list of definitions from other modules
which will be "pre-tagged" and are not subject to the usual restriction on tagging in the same
file as the declaration.

Note: The `extra` fields bypass the `validate` function -
we assume the builtins are also pre-validated.
 -/
Lean.registerTagAttributeExtra : Lean.Name →
  String →
    List Lean.Name →
      (optParam (Lean.Name → Lean.AttrM Unit) fun x => pure ()) →
        autoParam Lean.Name Lean.registerTagAttributeExtra._auto_1 → IO Lean.TagAttributeExtra
-- Lean.Meta.Tactic.Cases
/-- Given `dec : Decidable p`, split the goal in two subgoals: one containing the hypothesis `h : p` and another containing `h : ¬ p`.
 -/
Lean.MVarId.byCasesDec : Lean.MVarId →
  Lean.Expr → Lean.Expr → optParam Lean.Name `h → Lean.MetaM (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal)
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.sup_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f : Module.End R M} {p q : Submodule R M}, p ∈ f.invtSubmodule → q ∈ f.invtSubmodule → p ⊔ q ∈ f.invtSubmodule
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.compLeft_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v w : CategoryTheory.Arrow V} {f g : v ⟶ w} (h : CategoryTheory.Arrow.LeftHomotopy f g) (e : u ⟶ v),
  (h.compLeft e).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right e) h.hom
-- Mathlib.CategoryTheory.Limits.Preorder
/-- The cocone associated to an upper bound of a functor.  -/
Preorder.coconeOfUpperBound : {C : Type u} →
  [inst : Preorder C] →
    {J : Type u'} →
      [inst_1 : CategoryTheory.Category.{v, u'} J] →
        (F : CategoryTheory.Functor J C) → {x : C} → x ∈ upperBounds (Set.range F.obj) → CategoryTheory.Limits.Cocone F
-- Mathlib.GroupTheory.NoncommCoprod
MonoidHom.noncommCoprod_comp_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)),
  (f.noncommCoprod g comm).comp (MonoidHom.inl M N) = f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.eq_empty_iff_erase_eq_empty_and_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  (k : α), t = ∅ ↔ t.erase k = ∅ ∧ k ∉ t
-- Mathlib.Topology.Algebra.ConstMulAction
set_smul_closure_subset : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α] (s : Set M)
  (t : Set α), s • closure t ⊆ closure (s • t)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Restrict an affine simplex to an affine subspace that contains it.  -/
Affine.Simplex.restrict : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_5} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] →
            [inst_3 : AddTorsor V P] →
              {n : ℕ} →
                (s : Affine.Simplex k P n) →
                  (S : AffineSubspace k P) → (hS : affineSpan k (Set.range s.points) ≤ S) → Affine.Simplex k (↥S) n
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_eq_ofNat : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo] (m : α),
  ↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.leftDistribMulAction : {R : Type u_1} →
  {R' : Type u_4} →
    [inst : CommSemiring R] →
      [inst_1 : Monoid R'] →
        {M : Type u_7} →
          {N : Type u_8} →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : DistribMulAction R' M] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] → [SMulCommClass R R' M] → DistribMulAction R' (TensorProduct R M N)
-- Mathlib.Topology.LocallyConstant.Basic
/-- Evaluation/projection as a locally constant function.  -/
LocallyConstant.eval : {ι : Type u_5} →
  {X : ι → Type u_6} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      (i : ι) → [DiscreteTopology (X i)] → LocallyConstant ((i : ι) → X i) (X i)
-- Init.Data.Iterators.Basic
/-- If `it'` is obtained from `it` by skipping, then `Rel it' it`.  -/
Std.Iterators.ProductivenessRelation.subrelation : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  (self : Std.Iterators.ProductivenessRelation α m) {it it' : Std.IterM m β},
  it'.IsPlausibleSkipSuccessorOf it → self.Rel it' it
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.eq_of_edist_zero_on : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f f' : α → E} {s : Set α},
  (∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0) → eVariationOn f s = eVariationOn f' s
-- Mathlib.Order.Antichain
IsAntichain.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) (s : Set α), IsAntichain r s = s.Pairwise rᶜ
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getKeyD k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) fallback =
      if Std.Internal.List.containsKey k l₂ = true then Std.Internal.List.getKeyD k l₁ fallback else fallback
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
/-- If `f` sends `I` to `0` and `Iᶜ` to units, then `f` lifts to `κ(I)`.  -/
Ideal.ResidueField.lift : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (I : Ideal R) →
          [inst_2 : I.IsPrime] →
            (f : R →+* S) →
              I ≤ RingHom.ker f → I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S) → I.ResidueField →+* S
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Finsupp.basis_repr : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {φ : ι → Type u_4} (b : (i : ι) → Module.Basis (φ i) R M) (g : ι →₀ M) (ix : (i : ι) × φ i),
  ((Finsupp.basis b).repr g) ix = ((b ix.fst).repr (g ix.fst)) ix.snd
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
Filter.EventuallyEq.extDerivWithin_eq_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E}, ω₁ =ᶠ[nhds x] ω₂ → extDerivWithin ω₁ s x = extDerivWithin ω₂ s x
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.toNormedCommRing : {α : Type u_2} → [NormedField α] → NormedCommRing α
-- Lean.Parser.Attr
Lean.Parser.attrParser.parenthesizer : optParam ℕ 0 → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Action.Limits
Action.instSMulIntHom : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → [CategoryTheory.Preadditive V] → {X Y : Action V G} → SMul ℤ (X ⟶ Y)
-- Init.Data.Repr
instReprAtomUInt32 : ReprAtom UInt32
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- If `G` is cyclic of order `n` and `G'` contains a primitive `n`th root of unity,
then for each `a : G` with `a ≠ 1` there is a homomorphism `φ : G →* G'` such that `φ a ≠ 1`.  -/
IsCyclic.exists_apply_ne_one : ∀ {G : Type u_7} {G' : Type u_8} [inst : Group G] [IsCyclic G] [Finite G] [inst_3 : CommGroup G'],
  (∃ ζ, IsPrimitiveRoot ζ (Nat.card G)) → ∀ ⦃a : G⦄, a ≠ 1 → ∃ φ, φ a ≠ 1
-- Mathlib.Data.Matrix.Reflection
/-- `Matrix.mul` with better defeq for `Fin`  -/
Matrix.mulᵣ : {l m n : ℕ} →
  {α : Type u_1} →
    [Mul α] → [Add α] → [Zero α] → Matrix (Fin l) (Fin m) α → Matrix (Fin m) (Fin n) α → Matrix (Fin l) (Fin n) α
-- Lean.Meta.Basic
Lean.Meta.DefEqCacheKey.rhs : Lean.Meta.DefEqCacheKey → Lean.Expr
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Colex.orderBot : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [inst_1 : (i : ι) → AddCommMonoid (α i)] →
        [inst_2 : (i : ι) → PartialOrder (α i)] → [∀ (i : ι), IsBotZeroClass (α i)] → OrderBot (Colex (Π₀ (i : ι), α i))
-- Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Complex.arctan.eq_1 : ∀ (z : ℂ), z.arctan = -Complex.I / 2 * Complex.log ((1 + z * Complex.I) / (1 - z * Complex.I))
-- Init.Data.BitVec.Lemmas
BitVec.signExtend.eq_1 : ∀ {w : ℕ} (v : ℕ) (x : BitVec w), BitVec.signExtend v x = BitVec.ofInt v x.toInt
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsEisensteinAt.mk : ∀ {R : Type u} [inst : CommSemiring R] {f : Polynomial R} {𝓟 : Ideal R},
  f.leadingCoeff ∉ 𝓟 → (∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟) → f.coeff 0 ∉ 𝓟 ^ 2 → f.IsEisensteinAt 𝓟
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the spans of two pairs of vectors are equal, twice angles between those vectors are
equal.  -/
Orientation.two_zsmul_oangle_of_span_eq_of_span_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {w x y z : V}, ℝ ∙ w = ℝ ∙ x → ℝ ∙ y = ℝ ∙ z → 2 • o.oangle w y = 2 • o.oangle x z
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a normed group from a norm, i.e., registering the distance and the metric space
structure from the norm properties. Note that in most cases this instance creates bad definitional
equalities (e.g., it does not take into account a possibly existing `UniformSpace` instance on
`E`).  -/
GroupNorm.toNormedCommGroup : {E : Type u_5} → [inst : CommGroup E] → GroupNorm E → NormedCommGroup E
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.instantiateLevelParamsS : Lean.Expr → List Lean.Name → List Lean.Level → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.pure_seq : ∀ {α β : Type u} (f : α → β) (x : FreeAbelianGroup α), pure f <*> x = f <$> x
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.instBialgebra.eq_1 : ∀ (R : Type u_1) (A : Type u_3) (M : Type u_8) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : Monoid M],
  MonoidAlgebra.instBialgebra R A M =
    { toAlgebra := MonoidAlgebra.algebra, toCoalgebra := MonoidAlgebra.instCoalgebra R A M, counit_one := ⋯,
      mul_compr₂_counit := ⋯, comul_one := ⋯, mul_compr₂_comul := ⋯ }
-- Mathlib.SetTheory.Ordinal.Basic
InitialSeg.ordinal_type_le : ∀ {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s]
  (h : InitialSeg r s), Ordinal.type r ≤ Ordinal.type s
-- Mathlib.Analysis.LocallyConvex.Separation
/-- A version of the **Hahn-Banach theorem**: given disjoint convex sets `s`, `t` where `s` is open,
there is a continuous linear functional which separates them.  -/
geometric_hahn_banach_open : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s t : Set E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E],
  Convex ℝ s → IsOpen s → Convex ℝ t → Disjoint s t → ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.id_apply : ∀ {M : Type u_2} {X : Type u_5} [inst : VAdd M X] (x : X), (AddActionHom.id M) x = x
-- Init.Prelude
/-- A decision procedure for non-strict inequality of natural numbers, usually accessed via the
`DecidableLE Nat` instance.

Examples:
 * `(if 3 ≤ 4 then "yes" else "no") = "yes"`
 * `(if 6 ≤ 4 then "yes" else "no") = "no"`
 * `show 12 ≤ 12 by decide`
 * `show 5 ≤ 12 by decide`
 -/
Nat.decLe : (n m : ℕ) → Decidable (n ≤ m)
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.balanced_modify : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] {k : α} {f : β k → β k}
  {t : Std.DTreeMap.Internal.Impl α β}, t.Balanced → (Std.DTreeMap.Internal.Impl.modify k f t).Balanced
-- Lean.DocString.Extension
Lean.VersoDocString : Type
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- If there is a nonzero vector and every other vector is a multiple of it,
then the module has dimension one.  -/
rank_eq_one : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] [StrongRankCondition R] (v : M), v ≠ 0 → (∀ (w : M), ∃ c, c • v = w) → Module.rank R M = 1
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.fiberInclusion_obj_inj : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮}, Function.Injective CategoryTheory.Functor.Fiber.fiberInclusion.obj
-- Lean.Declaration
Lean.ConstantInfo.inductInfo.sizeOf_spec : ∀ (val : Lean.InductiveVal), sizeOf (Lean.ConstantInfo.inductInfo val) = 1 + sizeOf val
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
intervalIntegral.inv_mul_integral_comp_div_sub : ∀ {a b : ℝ} {f : ℝ → ℝ} (c d : ℝ), c⁻¹ * ∫ (x : ℝ) in a..b, f (x / c - d) = ∫ (x : ℝ) in a / c - d..b / c - d, f x
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.zpow'_of_ne_zero_left : ∀ {α : Type u_1} [inst : GroupWithZero α] (a : α) (n : ℤ), a ≠ 0 → Mathlib.Tactic.FieldSimp.zpow' a n = a ^ n