mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Category.BddLat
BddLat.Hom.ext_iff : ∀ {X Y : BddLat} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_self_apply : ∀ {α : Type u_2} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle] (x : α), f.cycleOf (f x) = f.cycleOf x
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlock.disjoint_smul_right : ∀ {M : Type u_1} {X : Type u_2} [inst : Monoid M] [inst_1 : MulAction M X] {B : Set X} {s : Set M},
  MulAction.IsBlock M B → ¬B ⊆ s • B → Disjoint B (s • B)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.sub_mem_orthogonal_of_inner_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} {x y : E}, (∀ (v : ↥K), inner 𝕜 x ↑v = inner 𝕜 y ↑v) → x - y ∈ Kᗮ
-- Mathlib.Data.Seq.Computation
Computation.instAlternativeComputation : Alternative Computation
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.IterM.length_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabDescr.mk.injEq : ∀
  (mkInductiveView mkInductiveView_1 :
    Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep1),
  ({ mkInductiveView := mkInductiveView } = { mkInductiveView := mkInductiveView_1 }) =
    (mkInductiveView = mkInductiveView_1)
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.posSemidef_covMatrix : ∀ (I : Finset NNReal), (ProbabilityTheory.BrownianReal.covMatrix I).PosSemidef
-- Mathlib.Order.Heyting.Hom
BiheytingHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : BiheytingAlgebra α} {inst_1 : BiheytingAlgebra β}
  {toLatticeHom : LatticeHom α β}
  {map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b}
  {map_sdiff' : ∀ (a b : α), toLatticeHom.toFun (a \ b) = toLatticeHom.toFun a \ toLatticeHom.toFun b}
  {toLatticeHom_1 : LatticeHom α β}
  {map_himp'_1 : ∀ (a b : α), toLatticeHom_1.toFun (a ⇨ b) = toLatticeHom_1.toFun a ⇨ toLatticeHom_1.toFun b}
  {map_sdiff'_1 : ∀ (a b : α), toLatticeHom_1.toFun (a \ b) = toLatticeHom_1.toFun a \ toLatticeHom_1.toFun b},
  { toLatticeHom := toLatticeHom, map_himp' := map_himp', map_sdiff' := map_sdiff' } =
      { toLatticeHom := toLatticeHom_1, map_himp' := map_himp'_1, map_sdiff' := map_sdiff'_1 } →
    toLatticeHom = toLatticeHom_1
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mem_carrier : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Subsemiring R} {x : R}, x ∈ s.carrier ↔ x ∈ s
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsColimitsOfShape J F
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.rightUnitor_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).hom
-- Mathlib.Analysis.Normed.Ring.Basic
NormMulClass.toNoZeroDivisors : ∀ {α : Type u_2} [inst : NormedRing α] [NormMulClass α], NoZeroDivisors α
-- Mathlib.Analysis.Calculus.ContDiff.Convolution
HasCompactSupport.hasDerivAt_convolution_left : ∀ {𝕜 : Type u𝕜} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] {f₀ : 𝕜 → E} {g₀ : 𝕜 → E'}
  (L : E →L[𝕜] E' →L[𝕜] F) {μ : MeasureTheory.Measure 𝕜} [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ]
  [μ.IsNegInvariant],
  HasCompactSupport f₀ →
    ContDiff 𝕜 1 f₀ →
      MeasureTheory.LocallyIntegrable g₀ μ →
        ∀ (x₀ : 𝕜), HasDerivAt (MeasureTheory.convolution f₀ g₀ L μ) (MeasureTheory.convolution (deriv f₀) g₀ L μ x₀) x₀
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.dual_id : ∀ {α : Type u_2} [inst : Min α] [inst_1 : Top α], InfTopHom.dual (InfTopHom.id α) = SupBotHom.id αᵒᵈ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.RankFunction.mk : {X : SSet} →
  {A : X.Subcomplex} →
    {h : A.PairingCore} →
      {α : Type v} →
        [inst : PartialOrder α] →
          (rank : h.ι → α) → (∀ {x y : h.ι}, h.AncestralRel x y → rank x < rank y) → h.RankFunction α
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- An algebra morphism with an underlying monomorphism hom in `C` is an algebra monomorphism.  -/
CategoryTheory.Endofunctor.Algebra.mono_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {X Y : CategoryTheory.Endofunctor.Algebra F} (f : X ⟶ Y) [h : CategoryTheory.Mono f.f], CategoryTheory.Mono f
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasSum.map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {a : α} {L : SummationFilter β} [inst_2 : AddCommMonoid γ] [inst_3 : TopologicalSpace γ],
  HasSum f a L →
    ∀ {G : Type u_4} [inst_4 : FunLike G α γ] [AddMonoidHomClass G α γ] (g : G), Continuous ⇑g → HasSum (⇑g ∘ f) (g a) L
-- Mathlib.Computability.Reduce
ManyOneDegree.of_le_of : ∀ {α : Type u} [inst : Primcodable α] [inst_1 : Inhabited α] {β : Type v} [inst_2 : Primcodable β]
  [inst_3 : Inhabited β] {p : α → Prop} {q : β → Prop}, ManyOneDegree.of p ≤ ManyOneDegree.of q ↔ p ≤₀ q
-- Init.Data.BitVec.Lemmas
BitVec.slt_zero_eq_msb : ∀ {w : ℕ} {x : BitVec w}, x.slt 0#w = x.msb
-- Init.Data.List.ToArray
/-- Variant of `foldlM_toArray` with a side condition for the `stop` argument.  -/
List.foldlM_toArray' : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {stop : ℕ} [inst : Monad m] (f : β → α → m β) (init : β)
  (l : List α), stop = l.toArray.size → Array.foldlM f init l.toArray 0 stop = List.foldlM f init l
-- Init.Data.Iterators.Combinators.Append
/-- Given two iterators `it₁` and `it₂`, `it₁.append it₂` is an iterator that first outputs all values
of `it₁` in order and then all values of `it₂` in order.

**Marble diagram:**

```text
it₁                 ---a----b---c--⊥
it₂                                 --d--e--⊥
it₁.append it₂      ---a----b---c-----d--e--⊥
```

**Termination properties:**

* `Finite` instance: only if `it₁` and `it₂` are finite
* `Productive` instance: only if `it₁` and `it₂` are productive

Note: If `it₁` is not finite, then `it₁.append it₂` can be productive while `it₂` is not.
The standard library does not provide a `Productive` instance for this case.

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it₁` and `it₂`.
 -/
Std.Iter.append : {α₁ α₂ β : Type w} → [Std.Iterator α₁ Id β] → [Std.Iterator α₂ Id β] → Std.Iter β → Std.Iter β → Std.Iter β
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.CotangentSpace.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'} {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'] (f f_1 : P.Hom P'),
  f = f_1 → Algebra.Extension.CotangentSpace.map f = Algebra.Extension.CotangentSpace.map f_1
-- Mathlib.Tactic.Translate.ToDual
/-- The global `do_translate`/`dont_translate` attributes specify whether operations on
a given type should be translated. `dont_translate` can be used for types that are translated,
such as `MonoidAlgebra` -> `AddMonoidAlgebra`, or for fixed types, such as `Fin n`/`ZMod n`.
`do_translate` is for types without arguments, like `Unit` and `Empty`, where the structure on it
can be translated.

Note: The name generation is not aware of `dont_translate`, so if some part of a lemma is not
  translated thanks to this, you generally have to specify the translated name manually.
 -/
Mathlib.Tactic.ToDual.to_dual_dont_translate : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.notMem_support_takeUntil_support_takeUntil_subset : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] {p : G.Walk u v} {x : V},
  x ≠ w → ∀ (hw : w ∈ p.support) (hx : x ∈ (p.takeUntil w hw).support), w ∉ (p.takeUntil x ⋯).support
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Option.getD.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : α) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match some x with
    | some x => h_1 x
    | none => h_2 ()) =
    h_1 x
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Measurable.sInf : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {ι : Type u_5} {f : ι → δ → α} {s : Set ι},
  s.Countable → (∀ i ∈ s, Measurable (f i)) → Measurable fun x => sInf ((fun i => f i x) '' s)
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.lt_def : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : PartialOrder β]
  {f g : C(α, β)}, f < g ↔ (∀ (a : α), f a ≤ g a) ∧ ∃ a, f a < g a
-- Mathlib.Algebra.Order.IsBotOne
pos_iff_ne_zero : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α], 0 < a ↔ a ≠ 0
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.posSemidef : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] {M : Matrix n n R},
  M.PosDef → M.PosSemidef
-- Std.Data.TreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.TreeMap.entryAtIdx! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap α β cmp → ℕ → α × β
-- Mathlib.Data.ZMod.IntUnitsPower
uzpow_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Module R (Additive ℤˣ)] (s : ℤˣ) (x : R), s ^ (-x) = (s ^ x)⁻¹
-- Batteries.Data.Fin.Basic
/-- Product of a tuple indexed by `Fin n`.  -/
Fin.prod : {α : Type u_1} → {n : ℕ} → [One α] → [Mul α] → (Fin n → α) → α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolInformation.mk.inj : ∀ {name : String} {kind : Lean.Lsp.SymbolKind} {tags : Array Lean.Lsp.SymbolTag} {location : Lean.Lsp.Location}
  {containerName? : Option String} {name_1 : String} {kind_1 : Lean.Lsp.SymbolKind} {tags_1 : Array Lean.Lsp.SymbolTag}
  {location_1 : Lean.Lsp.Location} {containerName?_1 : Option String},
  { name := name, kind := kind, tags := tags, location := location, containerName? := containerName? } =
      { name := name_1, kind := kind_1, tags := tags_1, location := location_1, containerName? := containerName?_1 } →
    name = name_1 ∧ kind = kind_1 ∧ tags = tags_1 ∧ location = location_1 ∧ containerName? = containerName?_1
-- Mathlib.Data.Set.Function
Set.LeftInvOn.injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {f₁' : β → α}, Set.LeftInvOn f₁' f s → Set.InjOn f s
-- Mathlib.Analysis.Calculus.Deriv.Inv
/-- Eta-expanded form of `DifferentiableAt.div` -/
DifferentiableAt.fun_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'},
  DifferentiableAt 𝕜 c x → DifferentiableAt 𝕜 d x → d x ≠ 0 → DifferentiableAt 𝕜 (fun i => c i / d i) x
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- Pick a presentation for an ind-object using choice.  -/
CategoryTheory.Limits.IsIndObject.presentation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      CategoryTheory.Limits.IsIndObject A → CategoryTheory.Limits.IndObjectPresentation A
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_left_eq_self : ∀ {w : ℕ} (a b : BitVec w), (a + b == b) = (a == 0#w)
-- Mathlib.Algebra.Order.Hom.Monoid
/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`.  -/
OrderMonoidIso.apply_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β) (y : β), e (e.symm y) = y
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₄Unchecked.eq_1 : ∀ (w x y z : UInt8),
  ByteArray.utf8DecodeChar?.assemble₄Unchecked w x y z =
    (w &&& 7).toUInt32 <<< 18 ||| (x &&& 63).toUInt32 <<< 12 ||| (y &&& 63).toUInt32 <<< 6 ||| (z &&& 63).toUInt32
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
NumberField.InfinitePlace.inertiaDeg_eq_one : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {w : NumberField.InfinitePlace L},
  w ∈ NumberField.InfinitePlace.unramifiedPlacesOver L v → v.inertiaDeg w = 1
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.instMonadStateOfStateClickSuggestionsM : MonadStateOf Mathlib.Tactic.ClickSuggestions.State Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.ins.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (parent : RBTree.RBNode.Path α) (y : α)
  (b a : RBTree.RBNode α) (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b) a)
  (h_3 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent) b)
  (h_4 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b) a)
  (h_5 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent) b),
  (match RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a => h_2 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b => h_3 a y parent b
    | RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a => h_4 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b => h_5 a y parent b) =
    h_2 parent y b a
-- Mathlib.Data.Int.Interval
Int.card_Ioo_of_lt : ∀ (a b : ℤ), a < b → ↑(Finset.Ioo a b).card = b - a - 1
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A}
  (H : g.IsWeierstrassFactorizationAt f h I) [inst_1 : IsAdicComplete I A],
  H.algEquivQuotient = ⋯.algEquivQuotient.trans (Ideal.quotientEquivAlgOfEq A ⋯)
-- Lean.Meta.Basic
Lean.Meta.withNewLocalInstances : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Array Lean.Expr → ℕ → n α → n α
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
lowerHemicontinuous_singleton_id : ∀ {α : Type u_1} [inst : TopologicalSpace α], LowerHemicontinuous fun x => {x}
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [inst_4 : CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.forget A).ReflectsIsomorphisms]
  [J.HasSheafCompose (CategoryTheory.forget A)]
  [∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)]
  [∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)],
  J.WEqualsLocallyBijective A
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_insert_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, (m.insert k v).getKey? k = some k
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
Fintype.not_linearIndependent_iffₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Fintype ι],
  ¬LinearIndependent R v ↔ ∃ f g, ∑ i, f i • v i = ∑ i, g i • v i ∧ ∃ i, f i ≠ g i
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict differentiability in the right endpoint.

If `f : ℝ → E` is continuous, then `u ↦ ∫ x in a..u, f x` has derivative `f b` at `b` in the sense
of strict differentiability.  -/
Continuous.integral_hasStrictDerivAt : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E},
  Continuous f → ∀ (a b : ℝ), HasStrictDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) (f b) b
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a fallback : α}, (m.insert k).getD a fallback = if (k == a) = true ∧ k ∉ m then k else m.getD a fallback
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- An object in `Fib p S` isomorphic in `𝒳` to a given object `a : 𝒳` such that `p(a) = S`.  -/
HasFibers.Fib.mk : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} → [inst_2 : HasFibers p] → {S : 𝒮} → {a : 𝒳} → p.obj a = S → HasFibers.Fib p S
-- Init.Data.Array.BinSearch
_private.Init.Data.Array.BinSearch.0.Array.binSearchAux.match_1.splitter : {α : Type u_1} →
  (as : Array α) →
    (motive : (x : Fin (as.size + 1)) → (x_1 : Fin as.size) → ↑x ≤ ↑x_1 → Sort u_2) →
      (x : Fin (as.size + 1)) →
        (x_1 : Fin as.size) →
          (x_2 : ↑x ≤ ↑x_1) →
            ((lo : Fin (as.size + 1)) → (hi : Fin as.size) → (h : ↑lo ≤ ↑hi) → motive lo hi h) → motive x x_1 x_2
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_one : ∀ {n : ℕ} {α : Fin (n + 2) → Sort u_1} (x : α 0) (p : (i : Fin n.succ) → α i.succ), Fin.cons x p 1 = p 0
-- Init.Grind.Offset
Lean.Grind.Nat.le_of_eq_1 : ∀ (u v : ℕ), u = v → u ≤ v
-- Mathlib.Data.Fin.SuccPred
Fin.coe_of_injective_castLE_symm : ∀ {n k : ℕ} (h : n ≤ k) (i : Fin k) (hi : i ∈ Set.range (Fin.castLE h)),
  ↑((Equiv.ofInjective (Fin.castLE h) ⋯).symm ⟨i, hi⟩) = ↑i
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.faceOpposite.eq_1 : ∀ {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 : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.faceOpposite i = s.face ⋯
-- Mathlib.Algebra.Order.Module.Defs
smul_min_of_nonneg : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : LinearOrder β]
  [inst_3 : Zero α] [PosSMulMono α β], 0 ≤ a → ∀ (b₁ b₂ : β), a • min b₁ b₂ = min (a • b₁) (a • b₂)
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.eq_comp_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {α : Type u_9} (e : M ≃+ N) (f : N → α) (g : M → α),
  f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.π.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  (s : CategoryTheory.Limits.WidePullbackCone f) (i : ι), s.π i = s.π.app (some i)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.mk : {R : Type u} →
  {M : Type v} →
    [inst : VAdd R M] → (carrier : Set M) → (∀ (c : R) {x : M}, x ∈ carrier → c +ᵥ x ∈ carrier) → SubAddAction R M
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.toPoly'.go.eq_3 : ∀ (coeff : ℤ) (a b : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Expr.toPoly'.go coeff (a.add b) =
    Lean.Grind.Linarith.Expr.toPoly'.go coeff a ∘ Lean.Grind.Linarith.Expr.toPoly'.go coeff b
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x : E), Meromorphic fun x_1 => x
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Composition of non-unital ring homomorphisms is associative.  -/
NonUnitalRingHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] {δ : Type u_5}
  {x : NonUnitalNonAssocSemiring δ} (f : α →ₙ+* β) (g : β →ₙ+* γ) (h : γ →ₙ+* δ), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.not_bddAbove_compl_of_small : ∀ (s : Set Ordinal.{u}) [hs : Small.{u, u + 1} ↑s], ¬BddAbove sᶜ
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
LieAddGroup.toContMDiffAdd : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} {inst_4 : AddGroup G} {inst_5 : TopologicalSpace G} {inst_6 : ChartedSpace H G}
  [self : LieAddGroup I n G], ContMDiffAdd I n G
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.suggestionName : Lean.Name → Lean.Elab.TermElabM Lean.Name
-- Lean.Util.FindMVar
Lean.Expr.findMVar? : Lean.Expr → (Lean.MVarId → Bool) → Option Lean.MVarId
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.ulift_obj_map : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D) (X : C) {X_1 Y : Dᵒᵖ} (f : X_1 ⟶ Y),
  ((CategoryTheory.Profunctor.ulift.{w', w, v₁, v₂, u₁, u₂} P).obj X).map f =
    TypeCat.ofHom fun x => { down := (CategoryTheory.ConcreteCategory.hom ((P.obj X).map f)) x.down }
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.IsLocalizationMap.map_units : ∀ {M : Type u_1} [inst : CommMonoid M] {N : Type u_2} [inst_1 : CommMonoid N] {S : Submonoid M} {f : M → N},
  S.IsLocalizationMap f → ∀ (y : ↥S), IsUnit (f ↑y)
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.singleton_set_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] (N : Submodule R M) [inst_5 : SMulCommClass S R M] (r : S),
  {r} • N = r • N
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_ne_top : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  {K : Ideal S} [inst_3 : RingHomClass F R S], K ≠ ⊤ → Ideal.comap f K ≠ ⊤