mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets.iIndepSet_of_mem : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ι → Set (Set Ω)} {f : ι → Set Ω},
  (∀ (i : ι), f i ∈ π i) →
    (∀ (i : ι), MeasurableSet (f i)) →
      ProbabilityTheory.Kernel.iIndepSets π κ μ → ProbabilityTheory.Kernel.iIndepSet f κ μ
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereographic'.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (n : ℕ)
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)),
  stereographic' n v =
    (stereographic ⋯).trans (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr.toHomeomorph.toOpenPartialHomeomorph
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitInclusiveIterator.toOption.eq_2 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice}, String.Slice.SplitInclusiveIterator.toOption✝ String.Slice.SplitInclusiveIterator.atEnd = none
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instIsNegApply : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_8 : IsTopologicalAddGroup M₂],
  IsNegApply (M →SL[σ₁₂] M₂) M M₂
-- Mathlib.Algebra.Lie.Solvable
LieIdeal.derivedSeries_succ_eq_top_iff : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (n : ℕ),
  LieAlgebra.derivedSeries R L (n + 1) = ⊤ ↔ LieAlgebra.derivedSeries R L 1 = ⊤
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.ringModuleOf_bracket_proj : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [inst_5 : IsLieAbelian M] (E : LieAlgebra.Extension R M L) (y : M)
  (z : E.L), ⁅E.proj z, y⁆ = E.toKer.symm ⁅z, E.toKer y⁆
-- Mathlib.GroupTheory.OrderOfElement
/-- **Alias** of the forward direction of `isOfFinAddOrder_iff_nsmul_eq_zero`. -/
IsOfFinAddOrder.exists_nsmul_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, IsOfFinAddOrder x → ∃ n, 0 < n ∧ n • x = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitOp.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y P : C} {f g : X ⟶ Y} (ι ι' : P ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
  (w' : CategoryTheory.CategoryStruct.comp f.op ι'.op = CategoryTheory.CategoryStruct.comp g.op ι'.op) (h : ι = ι'),
  CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitOp ι ι' w w' h =
    CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitOp ι ι' w w' h
-- Mathlib.Order.Filter.Germ.Basic
/-- A germ at `l` of maps from `α` to `β` tends to `lb : Filter β` if it is represented by a map
which tends to `lb` along `l`.  -/
Filter.Germ.Tendsto : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → l.Germ β → Filter β → Prop
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- If a sequence of bounded continuous functions tends to the indicator of a measurable set and
the functions are uniformly bounded, then their integrals against a finite measure tend to the
measure of the set.

A similar result with more general assumptions is
`MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicator`.
 -/
MeasureTheory.measure_of_cont_bdd_of_tendsto_indicator : ∀ {Ω : Type u_1} [inst : TopologicalSpace Ω] [inst_1 : MeasurableSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {c : NNReal} {E : Set Ω},
  MeasurableSet E →
    ∀ (fs : ℕ → BoundedContinuousFunction Ω NNReal),
      (∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c) →
        Filter.Tendsto (fun n ω => (fs n) ω) Filter.atTop (nhds (E.indicator fun x => 1)) →
          Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) Filter.atTop (nhds (μ E))
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.step.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  (l : Λ) (v : σ) (S : (k : K) → List (Γ k)),
  Turing.TM2.step M { l := some l, var := v, stk := S } = some (Turing.TM2.stepAux (M l) v S)
-- Mathlib.Order.InitialSeg
InitialSeg.toOrderEmbedding_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α ≤i β) (x : α),
  f.toOrderEmbedding x = f x
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.continuous : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → Continuous f
-- Mathlib.Data.Bool.Basic
Bool.toNat_bne_one : ∀ (b : Bool), (b.toNat != 1) = !b
-- Mathlib.CategoryTheory.Category.Quiv
/-- A prefunctor `V ⥤q W` induces a functor between the path categories defined by `F.mapPath`.  -/
CategoryTheory.Cat.freeMap : {V : Type u_1} →
  {W : Type u_2} →
    [inst : Quiver V] →
      [inst_1 : Quiver W] → V ⥤q W → CategoryTheory.Functor (CategoryTheory.Paths V) (CategoryTheory.Paths W)
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_zero_right`.  -/
hammingDist_zero_right : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)] (x : (i : ι) → β i), hammingDist x 0 = hammingNorm x
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_unique : ∀ {ι : Type u_3} [inst : Unique ι] (f : ι → Ordinal.{max u_4 u_3}), Ordinal.lsub f = Order.succ (f default)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.pointwiseRightKanExtension_map : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseRightKanExtension F]
  {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂),
  (L.pointwiseRightKanExtension F).map f =
    CategoryTheory.Limits.limit.lift ((CategoryTheory.StructuredArrow.proj Y₂ L).comp F)
      { pt := CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y₁ L).comp F),
        π :=
          {
            app := fun g =>
              CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y₁ L).comp F)
                ((CategoryTheory.StructuredArrow.map f).obj g),
            naturality := ⋯ } }
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_inverse_obj_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRightIso L i).inverse.obj X).hom =
    CategoryTheory.CategoryStruct.comp X.hom (i.inv.app X.right)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_id_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Z : C} {f : X ⟶ Z},
  CategoryTheory.IsPullback f (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Z) f
-- Mathlib.Data.WSeq.Relation
_private.Mathlib.Data.WSeq.Relation.0.Stream'.WSeq.destruct_join.aux.match_1.splitter : {α : Type u_1} →
  (motive : Option (Stream'.WSeq α × Stream'.WSeq (Stream'.WSeq α)) → Sort u_2) →
    (x : Option (Stream'.WSeq α × Stream'.WSeq (Stream'.WSeq α))) →
      (Unit → motive none) →
        ((s : Stream'.WSeq α) → (S : Stream'.WSeq (Stream'.WSeq α)) → motive (some (s, S))) → motive x
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pos.revSkipWhile.induct_unfolding : ∀ {ρ : Type} {s : String.Slice} (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat]
  (motive : s.Pos → s.Pos → Prop),
  (∀ (x nextCurr : s.Pos),
      x.revSkip? pat = some nextCurr →
        nextCurr < x → motive nextCurr (nextCurr.revSkipWhile pat) → motive x (nextCurr.revSkipWhile pat)) →
    (∀ (x nextCurr : s.Pos), x.revSkip? pat = some nextCurr → ¬nextCurr < x → motive x x) →
      (∀ (x : s.Pos), x.revSkip? pat = none → motive x x) → ∀ (pos : s.Pos), motive pos (pos.revSkipWhile pat)
-- Batteries.Lean.Meta.DiscrTree
/-- Merge two `Trie`s. Duplicate values are preserved.
 -/
Lean.Meta.DiscrTree.Trie.mergePreservingDuplicates : {α : Type} → Lean.Meta.DiscrTree.Trie α → Lean.Meta.DiscrTree.Trie α → Lean.Meta.DiscrTree.Trie α
-- Std.Time.Date.Basic
/-- Convert `Day.Offset` into `Nanosecond.Offset`.
 -/
Std.Time.Nanosecond.Offset.ofDays : Std.Time.Day.Offset → Std.Time.Nanosecond.Offset
-- Lean.Data.Options
Lean.Option.Decl.mk : {α : Type} → α → String → Option Lean.OptionDeprecation → Lean.Option.Decl α
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.instIsGeneratedByCarrierObjTopCatGeneratedBy : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] (Y : GeneratedByTopCat X),
  Topology.IsGeneratedBy X ↑Y.obj
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.hasLimit_parallelPair : ∀ {V W : SemiNormedGrp} (f g : V ⟶ W), CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)
-- Mathlib.RingTheory.WittVector.StructurePolynomial
wittStructureInt_existsUnique : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ),
  ∃! φ,
    ∀ (n : ℕ),
      (MvPolynomial.bind₁ φ) (wittPolynomial p ℤ n) =
        (MvPolynomial.bind₁ fun i => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p ℤ n)) Φ
-- Mathlib.Analysis.Oscillation
ContinuousWithinAt.oscillationWithin_eq_zero : ∀ {E : Type u} {F : Type v} [inst : PseudoEMetricSpace F] [inst_1 : TopologicalSpace E] {f : E → F} {D : Set E} {x : E},
  ContinuousWithinAt f D x → oscillationWithin f D x = 0
-- Mathlib.RingTheory.Localization.Basic
Localization.algEquiv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (a : Localization M),
  (Localization.algEquiv M S) a = (IsLocalization.map S (RingHom.id R) ⋯) a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_eq_add_iff_eq_and_eq : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] {a b c d : α},
  a ≤ c → b ≤ d → (a + b = c + d ↔ a = c ∧ b = d)
-- Mathlib.Order.Partition.Finpartition
Finpartition.bind_parts : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α] {a : α}
  (P : Finpartition a) (Q : (i : α) → i ∈ P.parts → Finpartition i),
  (P.bind Q).parts = P.parts.attach.biUnion fun i => (Q ↑i ⋯).parts
-- Mathlib.Analysis.Calculus.FDeriv.Congr
/-- In the case `y = x`, see also `differentiableWithinAt_congr_set_nhdsNE`,
which does not require the domain to be a T₁ space.  -/
differentiableWithinAt_congr_set' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s t : Set E} [T1Space E] (y : E),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → (DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x)
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.shiftIso_add_inv_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n m a a' a'' : A) (ha' : n + a = a')
  (ha'' : m + a' = a'') (X : C),
  (F.shiftIso (m + n) a a'' ⋯).inv.app X =
    CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X))
        ((CategoryTheory.shiftFunctorAdd D m n).inv.app ((F.functor a'').obj X)))
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.coe_mapRingHom : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α] [inst_3 : IsUniformAddGroup α]
  {β : Type u} [inst_4 : UniformSpace β] [inst_5 : Ring β] [inst_6 : IsUniformAddGroup β] [inst_7 : IsTopologicalRing β]
  (f : α →+* β) (hf : Continuous ⇑f), ⇑(UniformSpace.Completion.mapRingHom f hf) = UniformSpace.Completion.map ⇑f
-- Init.Data.Int.Lemmas
Int.add_comm : ∀ (a b : ℤ), a + b = b + a
-- Mathlib.Analysis.CStarAlgebra.Unitary.Span
selfAdjoint.realPart_unitarySelfAddISMul : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (a : ↥(selfAdjoint A))
  (ha_norm : ‖a‖ ≤ 1), realPart ↑(selfAdjoint.unitarySelfAddISMul a ha_norm) = a
-- Mathlib.Algebra.Lie.IdealOperations
LieIdeal.map_bracket_eq : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') {I₁ I₂ : LieIdeal R L},
  Function.Surjective ⇑f → LieIdeal.map f ⁅I₁, I₂⁆ = ⁅LieIdeal.map f I₁, LieIdeal.map f I₂⁆
-- Mathlib.Data.Finset.Basic
Finset.insert_inter_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (a : α), insert a (s ∩ t) = insert a s ∩ insert a t
-- Mathlib.RingTheory.Valuation.Basic
Valuation.restrict_lt_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v.restrict x < v.restrict y ↔ v x < v y
-- Mathlib.Topology.Instances.ENat
ENat.instContinuousAdd : ContinuousAdd ℕ∞
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.CasesTypes.mk.inj : ∀ {casesMap casesMap_1 : Lean.PHashMap Lean.Name Bool},
  { casesMap := casesMap } = { casesMap := casesMap_1 } → casesMap = casesMap_1
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_dvd_of_le_left : ∀ {E : Type v} [inst : Field E] {A B : Subfield E} (C : Subfield E), A ≤ B → B.relrank C ∣ A.relrank C
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `AddEquiv.symm` defines an equivalence between `α ≃+ β` and `β ≃+ α`  -/
AddEquiv.symmEquiv : (P : Type u_9) → (Q : Type u_10) → [inst : Add P] → [inst_1 : Add Q] → P ≃+ Q ≃ (Q ≃+ P)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_sub_int_mul_two_pi : ∀ (x : ℂ) (n : ℤ), Complex.cos (x - ↑n * (2 * ↑Real.pi)) = Complex.cos x
-- Mathlib.Computability.TuringDegree
/-- `f` is Turing reducible to `g` if `f` is partial recursive given access to the oracle `g`
 -/
Computability.«term_≤ᵀ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- Let `F` be a functor from sheaf of `R`-module to sheaf of `S`-module, if `F` preserves
colimits and `F.obj (unit R) ≅ unit S`, given a `P : Presentation M`, then we will obtain
relations of `Presentation (F.obj M)`.  -/
SheafOfModules.Presentation.mapRelations : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {C' : Type u₂} →
              [inst_3 : CategoryTheory.Category.{v₂, u₂} C'] →
                {J' : CategoryTheory.GrothendieckTopology C'} →
                  {S : CategoryTheory.Sheaf J' RingCat} →
                    [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] →
                      [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat] →
                        {M : SheafOfModules R} →
                          (P : M.Presentation) →
                            (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) →
                              [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂,
                                      max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
                                    F] →
                                (SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) →
                                  (SheafOfModules.free P.relations.I ⟶ SheafOfModules.free P.generators.I)
-- Init.Data.Ord.Basic
Ordering.gt_then : ∀ {o : Ordering}, Ordering.gt.then o = Ordering.gt
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.epi_desc_of_epi_left : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [CategoryTheory.Epi f],
  CategoryTheory.Epi (CategoryTheory.Limits.biprod.desc f g)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_compTendsto : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (b : β) {lc : Filter γ} {g : γ → α}
  (hg : Filter.Tendsto g lc l), (↑b).compTendsto g hg = ↑b
-- Mathlib.Order.WithBot
WithTop.map_eq_top_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : WithTop α}, WithTop.map f a = ⊤ ↔ a = ⊤
-- Mathlib.RingTheory.MatrixAlgebra
/-- (Implementation detail.)

The bare function `Matrix n n A → A ⊗[R] Matrix n n R`.
(We don't need to show that it's an algebra map, thankfully --- just that it's an inverse.)
 -/
MatrixEquivTensor.invFun : (n : Type u_3) →
  (R : Type u_5) →
    (A : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [DecidableEq n] → [Fintype n] → Matrix n n A → TensorProduct R A (Matrix n n R)
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.neg : ∀ {R : Type u} {X : Type v} [inst : CommRing R] {a b : FreeNonUnitalNonAssocAlgebra R X},
  FreeLieAlgebra.Rel R X a b → FreeLieAlgebra.Rel R X (-a) (-b)
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.Int.smul_eq_mul : ∀ {R : Type u_2} {n n' : ℤ} {r : R} [inst : CommRing R], ↑n = r → n' = n → ∀ (a : R), n' • a = r * a
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PathObject.RightHomotopy.rightHomotopyRel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {X Y : C} {f g : X ⟶ Y} {P : HomotopicalAlgebra.PathObject Y} (h : P.RightHomotopy f g),
  HomotopicalAlgebra.RightHomotopyRel f g
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comapOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (N : Matroid β) (E : Set α) (f : α → β), N.comapOn E f = (N.comap f).restrict E
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Stats.mk : Lean.Meta.Simp.UsedSimps → Lean.Meta.Simp.Diagnostics → Lean.Meta.Simp.Stats
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.mk.inj : ∀ {J : CategoryTheory.Limits.MultispanShape} {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {left : J.L → C}
  {right : J.R → C} {fst : (a : J.L) → left a ⟶ right (J.fst a)} {snd : (a : J.L) → left a ⟶ right (J.snd a)}
  {left_1 : J.L → C} {right_1 : J.R → C} {fst_1 : (a : J.L) → left_1 a ⟶ right_1 (J.fst a)}
  {snd_1 : (a : J.L) → left_1 a ⟶ right_1 (J.snd a)},
  { left := left, right := right, fst := fst, snd := snd } =
      { left := left_1, right := right_1, fst := fst_1, snd := snd_1 } →
    left = left_1 ∧ right = right_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.instSemilatticeSup.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E],
  AddGroupNorm.instSemilatticeSup = Function.Injective.semilatticeSup DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.Order.Hom.Basic
OrderHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f g : α →o β}, f = g ↔ ⇑f = ⇑g
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A vector is in the `vectorSpan` of an indexed family if and only
if it is a `weightedVSub` with sum of weights 0.  -/
mem_vectorSpan_iff_eq_weightedVSub : ∀ {ι : Type u_1} (k : Type u_2) {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] {v : V} {p : ι → P},
  v ∈ vectorSpan k (Set.range p) ↔ ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_eq_some_iff_exists_beq_and_mem_toArray : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {k : α} {v : β}, m.WF → (m.get? k = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ m.toArray)
-- Mathlib.Algebra.Lie.Basic
LieEquiv.ext_iff : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] {f g : L₁ ≃ₗ⁅R⁆ L₂}, f = g ↔ ∀ (x : L₁), f x = g x
-- Mathlib.Order.CompleteLattice.Basic
iSup_mono : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f g : ι → α}, (∀ (i : ι), f i ≤ g i) → iSup f ≤ iSup g
-- Init.Data.Array.Attach
Array.toList_unattach : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }}, xs.unattach.toList = xs.toList.unattach
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.instFastIsEmptyFinOfNatNat : Lean.Meta.FastIsEmpty (Fin 0)
-- Mathlib.Data.Finset.Grade
/-- **Alias** of the reverse direction of `Finset.val_wcovBy_val`. -/
WCovBy.finset_val : ∀ {α : Type u_1} {s t : Finset α}, s ⩿ t → s.val ⩿ t.val
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanDidOpenTextDocumentParams.mk.inj : ∀ {toDidOpenTextDocumentParams : Lean.Lsp.DidOpenTextDocumentParams}
  {dependencyBuildMode? : Option Lean.Lsp.DependencyBuildMode}
  {toDidOpenTextDocumentParams_1 : Lean.Lsp.DidOpenTextDocumentParams}
  {dependencyBuildMode?_1 : Option Lean.Lsp.DependencyBuildMode},
  { toDidOpenTextDocumentParams := toDidOpenTextDocumentParams, dependencyBuildMode? := dependencyBuildMode? } =
      { toDidOpenTextDocumentParams := toDidOpenTextDocumentParams_1, dependencyBuildMode? := dependencyBuildMode?_1 } →
    toDidOpenTextDocumentParams = toDidOpenTextDocumentParams_1 ∧ dependencyBuildMode? = dependencyBuildMode?_1
-- Mathlib.Topology.Separation.GDelta
T6Space.toT0Space : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T6Space X], T0Space X
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharNeTwoNF_t : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : Invertible 2], W.toCharNeTwoNF.t = ⅟2 * -W.a₃
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.instHasHomotopyCofiberOppositeLiftSymmIdOpNegHomOfHasPathObject : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c)
  [inst_2 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [K.HasPathObject],
  HomologicalComplex.HasHomotopyCofiber
    (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K.op) (-CategoryTheory.CategoryStruct.id K.op))
-- Mathlib.Order.WellFounded
StrictMono.not_bddAbove_range_of_wellFoundedLT : ∀ {β : Type u_2} [inst : LinearOrder β] {f : β → β} [WellFoundedLT β] [NoMaxOrder β],
  StrictMono f → ¬BddAbove (Set.range f)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.algebraMap_eq_inlRingHom_comp : ∀ (S : Type u_1) (R : Type u_2) (A : Type u_3) [inst : CommSemiring S] [inst_1 : CommSemiring R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] [inst_5 : SMulCommClass R A A]
  [inst_6 : Algebra S R] [inst_7 : DistribMulAction S A] [inst_8 : IsScalarTower S R A],
  algebraMap S (Unitization R A) = (Unitization.inlRingHom R A).comp (algebraMap S R)
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.inclusion_right : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H K : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G]
  [inst_3 : LE S] [inst_4 : IsConcreteLE S G] (h : H ≤ K) (x : ↥K) (hx : ↑x ∈ H),
  (SubgroupClass.inclusion h) ⟨↑x, hx⟩ = x
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.hom_id : ∀ {R : Type u} [inst : CommRing R] {A : CommBialgCat R},
  CommBialgCat.Hom.hom (CategoryTheory.CategoryStruct.id A) = BialgHom.id R ↑A