mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given `CommMonoid`s `M, P` and Submonoids `S ⊆ M, T ⊆ P`, if `f : M →* N` is a Localization
map for `S` and `k : P ≃* M` is an isomorphism of `CommMonoid`s such that `k(T) = S`, `f ∘ k`
is a Localization map for `T`.  -/
Submonoid.LocalizationMap.ofMulEquivOfDom : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {N : Type u_2} →
        [inst_1 : CommMonoid N] →
          {P : Type u_3} →
            [inst_2 : CommMonoid P] →
              S.LocalizationMap N →
                {T : Submonoid P} → {k : P ≃* M} → Submonoid.map k.toMonoidHom T = S → T.LocalizationMap N
-- Mathlib.CategoryTheory.ObjectProperty.Basic
/-- The property of objects that is satisfied by the `X i` for a family
of objects `X : ι : C`.  -/
CategoryTheory.ObjectProperty.ofObj : {C : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] → {ι : Type u'} → (ι → C) → CategoryTheory.ObjectProperty C
-- Mathlib.GroupTheory.OrderOfElement
pow_mod_orderOf : ∀ {G : Type u_1} [inst : Monoid G] (x : G) (n : ℕ), x ^ (n % orderOf x) = x ^ n
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_mapWithPostcondition_eq_toArray_filterMapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [LawfulMonad n] [inst_4 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n γ} {it : Std.IterM m β},
  (Std.IterM.mapWithPostcondition f it).toArray =
    (Std.IterM.filterMapWithPostcondition (fun x => Std.Iterators.PostconditionT.map some (f x)) it).toArray
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.domRestrict_eq_zero_iff : ∀ {M : Type u_1} [inst : AddZeroClass M] {N : Type u_5} {S : Type u_6} [inst_1 : AddZeroClass N] {f : M →+ N}
  [inst_2 : SetLike S M] [inst_3 : AddSubmonoidClass S M] {s : S}, f.domRestrict s = 0 ↔ ∀ x ∈ s, f x = 0
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Define `PreInnerProductSpace.Core` from `InnerProductSpace`. Defined to reuse lemmas about
`PreInnerProductSpace.Core` for `PreInnerProductSpace`s. Note that the `Seminorm` instance provided
by `PreInnerProductSpace.Core.norm` is propositionally but not definitionally equal to the original
norm.  -/
PreInnerProductSpace.toCore : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [c : InnerProductSpace 𝕜 E] → PreInnerProductSpace.Core 𝕜 E
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.testAgainstNN_add : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.FiniteMeasure Ω) (f₁ f₂ : BoundedContinuousFunction Ω NNReal),
  μ.testAgainstNN (f₁ + f₂) = μ.testAgainstNN f₁ + μ.testAgainstNN f₂
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkStackTop.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.measure_eq_zero_or_one_of_indepSet_self : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {t : Set Ω},
  ProbabilityTheory.IndepSet t t μ → μ t = 0 ∨ μ t = 1
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntry.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
      false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2).isEmpty =
                              false) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)
                            h),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1, h with
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_1 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
      h_3 => h_2 size k v l size_2 k_2 v_2 l_1 r h r_2 h_3) =
    h_2 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 h
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sInf_neg : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M] (s : Set M),
  sInf (-s) = -sSup s
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.div_one : ∀ {R : Type u} [inst : EuclideanDomain R] (p : R), p / 1 = p
-- Mathlib.RingTheory.Unramified.Dedekind
isDedekindDomainDvr.of_formallyUnramified : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [Module.Finite A B]
  [IsDedekindDomain A] [inst_5 : IsDomain B] [Algebra.FormallyUnramified A B], IsDedekindDomainDvr B
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.RingObjCat C} {f g : R₁ ⟶ R₂},
  f = g ↔ f.hom = g.hom
-- Mathlib.Order.BoundedOrder.Basic
Pi.instOrderBot : {ι : Type u_1} →
  {α' : ι → Type u_2} → [inst : (i : ι) → LE (α' i)] → [(i : ι) → OrderBot (α' i)] → OrderBot ((i : ι) → α' i)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.chaar_sup_eq : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {K₁ K₂ : TopologicalSpace.Compacts G},
  Disjoint K₁.carrier K₂.carrier →
    IsClosed K₂.carrier →
      MeasureTheory.Measure.haar.chaar K₀ (K₁ ⊔ K₂) =
        MeasureTheory.Measure.haar.chaar K₀ K₁ + MeasureTheory.Measure.haar.chaar K₀ K₂
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RooSliceData.mk.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Roo α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α β) (range_1 : Std.Roo α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.IsRationalOver.mk : ∀ {S X : AlgebraicGeometry.Scheme} {sX : X ⟶ S},
  (∃ n, AlgebraicGeometry.Scheme.BirationalOver sX (AlgebraicGeometry.AffineSpace n S ↘ S)) →
    AlgebraicGeometry.Scheme.IsRationalOver sX
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_le_left : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G) [H₁.Normal], ⁅H₁, H₂⁆ ≤ H₁
-- Mathlib.Logic.Nontrivial.Defs
Nontrivial.mk : ∀ {α : Type u_3}, (∃ x y, x ≠ y) → Nontrivial α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget.h : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {combined : ℕ}
  (self : Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget aig combined), combined = self.w * self.n
-- Mathlib.Topology.UnitInterval
/-- like `unitInterval.nonneg`, but with the inequality in `I`.  -/
unitInterval.nonneg' : ∀ {t : ↑unitInterval}, 0 ≤ t
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.ext₅ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  (h₀ : f.obj' 0 _proof_449✝ = g.obj' 0 _proof_449✝) (h₁ : f.obj' 1 _proof_450✝ = g.obj' 1 _proof_450✝)
  (h₂ : f.obj' 2 _proof_451✝ = g.obj' 2 _proof_451✝) (h₃ : f.obj' 3 _proof_452✝ = g.obj' 3 _proof_452✝)
  (h₄ : f.obj' 4 _proof_453✝ = g.obj' 4 _proof_453✝) (h₅ : f.obj' 5 _proof_454✝ = g.obj' 5 _proof_454✝),
  f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝ =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀)
        (CategoryTheory.CategoryStruct.comp (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝)
          (CategoryTheory.eqToHom ⋯)) →
    f.map' 1 2 _proof_246✝ _proof_451✝ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁)
          (CategoryTheory.CategoryStruct.comp (g.map' 1 2 _proof_246✝ _proof_451✝) (CategoryTheory.eqToHom ⋯)) →
      f.map' 2 3 _proof_299✝ _proof_452✝ =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂)
            (CategoryTheory.CategoryStruct.comp (g.map' 2 3 _proof_299✝ _proof_452✝) (CategoryTheory.eqToHom ⋯)) →
        f.map' 3 4 _proof_364✝ _proof_453✝ =
            CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₃)
              (CategoryTheory.CategoryStruct.comp (g.map' 3 4 _proof_364✝ _proof_453✝) (CategoryTheory.eqToHom ⋯)) →
          f.map' 4 5 _proof_453✝ _proof_454✝ =
              CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₄)
                (CategoryTheory.CategoryStruct.comp (g.map' 4 5 _proof_453✝ _proof_454✝) (CategoryTheory.eqToHom ⋯)) →
            f = g
-- Mathlib.LinearAlgebra.Matrix.Permutation
Matrix.permMatrix_mul : ∀ {n : Type u_1} {R : Type u_2} [inst : DecidableEq n] (σ τ : Equiv.Perm n) [inst_1 : Fintype n]
  [inst_2 : NonAssocSemiring R], Equiv.Perm.permMatrix R (σ * τ) = Equiv.Perm.permMatrix R τ * Equiv.Perm.permMatrix R σ
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.coe_pi : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] (I : Set ι)
  (S : (i : ι) → AddSubmonoid (M i)), ↑(AddSubmonoid.pi I S) = I.pi fun i => ↑(S i)
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₁₃_obj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (G : C₃) (H : C₂) {X Y : C₁}
  (f : X ⟶ Y), ((F.flip₁₃.obj G).obj H).map f = ((F.map f).app H).app G
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.inclusion_right : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} {H K : S} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G]
  [inst_3 : LE S] [inst_4 : IsConcreteLE S G] (h : H ≤ K) (x : ↥K) (hx : ↑x ∈ H),
  (AddSubgroupClass.inclusion h) ⟨↑x, hx⟩ = x
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `TopologicalSpace.generatedBy_generatedBy`. -/
deltaGenerated_deltaGenerated_eq : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] (Y : Type u_1) [inst_1 : TopologicalSpace Y],
  TopologicalSpace.generatedBy X = TopologicalSpace.generatedBy X
-- Mathlib.Order.Interval.Set.OrdConnected
Set.image_subtype_val_uIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} [s.OrdConnected] (a b : ↑s),
  Subtype.val '' Set.uIcc a b = Set.uIcc ↑a ↑b
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.eq_toIterM_iter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (it : Std.Iter ((a : α) × β a)),
  it.toIterM = { internalState := it.internalState }
-- Mathlib.Util.CompileInductive
_private.Mathlib.Util.CompileInductive.0.Mathlib.Util.replaceConst : Lean.AssocList Lean.Name Lean.Name → Lean.Expr → Lean.Expr
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
/-- the rank function  -/
SSet.Subcomplex.PairingCore.RankFunction.rank : {X : SSet} →
  {A : X.Subcomplex} → {h : A.PairingCore} → {α : Type v} → [inst : PartialOrder α] → h.RankFunction α → h.ι → α
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- **Alias** of `CategoryTheory.ConcreteCategory.instFunLike`.

---

A non-instance `FunLike` instance on `X ⟶ Y`.  -/
CategoryTheory.HasForget.instFunLike : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {X Y : C} → FunLike (X ⟶ Y) (CategoryTheory.ToType X) (CategoryTheory.ToType Y)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.st_inv : ∀ (x : ℝ*), x⁻¹.st = x.st⁻¹
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapBifunctorBifunctor₂₃Desc_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [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} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r}
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] {j : J} {A : C₄}
  (f :
    (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ A))
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j) {Z : C₄} (h_1 : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃Desc f) h_1) =
    CategoryTheory.CategoryStruct.comp (f i₁ i₂ i₃ h) h_1
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.union_indep_iff_indep_of_subset_coloops : ∀ {α : Type u_1} {M : Matroid α} {I K : Set α}, K ⊆ M.coloops → (M.Indep (I ∪ K) ↔ M.Indep I)
-- Mathlib.NumberTheory.Divisors
Int.mem_divisorsAntidiag : ∀ {xy : ℤ × ℤ} {z : ℤ}, xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.map_id_comp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ),
  groupHomology.map (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n =
    CategoryTheory.CategoryStruct.comp (groupHomology.map (MonoidHom.id G) φ n) (groupHomology.map (MonoidHom.id G) ψ n)
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
/-- Every terminating continued fraction corresponds to a rational number.  -/
GenContFract.exists_rat_eq_of_terminates : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K},
  (GenContFract.of v).Terminates → ∃ q, v = ↑q
-- Mathlib.Data.Setoid.Partition
IndexedPartition.exists_mem : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α), ∃ i, x ∈ s i
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.paths_le_inverseImage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [W.IsMultiplicative], W.paths ≤ W.inverseImage (CategoryTheory.pathComposition C)
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.iIsOrtho_def : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : Type w}
  {B : LinearMap.BilinForm R M} {v : n → M}, B.iIsOrtho v ↔ ∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LEquiv.onTerm_symm_apply : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L ≃ᴸ L') (a : L'.Term α),
  φ.onTerm.symm a = φ.invLHom.onTerm a
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
_private.Mathlib.Algebra.Homology.Embedding.ExtendHomotopy.0.Homotopy.extend.homAux.match_1.eq_2 : ∀ {ι : Type u_1} (motive : Option ι → Option ι → Sort u_2) (x : Option ι) (h_1 : (x : Option ι) → motive none x)
  (h_2 : (x : Option ι) → motive x none) (h_3 : (i j : ι) → motive (some i) (some j)),
  (x = none → False) →
    (match x, none with
      | none, x => h_1 x
      | x, none => h_2 x
      | some i, some j => h_3 i j) =
      h_2 x
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mk_of_notMem : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {s : Finset ι}
  {x : (i : ↑↑s) → β ↑i} {i : ι}, i ∉ s → (DFinsupp.mk s x) i = 0
-- Mathlib.Order.Ideal
Order.Ideal.principal_bot : ∀ {P : Type u_1} [inst : Preorder P] [inst_1 : OrderBot P], Order.Ideal.principal ⊥ = ⊥
-- Mathlib.NumberTheory.SumPrimeReciprocals
/-- The sum over the reciprocals of the primes diverges.  -/
not_summable_one_div_on_primes : ¬Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List (List α) → Array α → Sort u_2) (x y : List α) (xs : List (List α))
  (acc : Array α) (h_1 : (x : List α) → (acc : Array α) → motive x [] acc)
  (h_2 : (x y : List α) → (xs : List (List α)) → (acc : Array α) → motive x (y :: xs) acc),
  (match x, y :: xs, acc with
    | x, [], acc => h_1 x acc
    | x, y :: xs, acc => h_2 x y xs acc) =
    h_2 x y xs acc
-- Mathlib.Topology.Perfect
PerfectSpace.not_isolated : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PerfectSpace X] (x : X), (nhdsWithin x {x}ᶜ).NeBot
-- Mathlib.Data.WSeq.Defs
/-- Map the elements of `s` over `f`, removing any values that yield `none`.  -/
Stream'.WSeq.filterMap : {α : Type u} → {β : Type v} → (α → Option β) → Stream'.WSeq α → Stream'.WSeq β
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_finsetSum_measure : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {f : α → E} {ι : Type u_7}
  {s : Finset ι} (hs : s.Nonempty) {μ : ι → MeasureTheory.Measure α} {T : ι → Set α → E →L[ℝ] F} {C : ι → ℝ}
  (hTs : ∀ (i : ι), MeasureTheory.DominatedFinMeasAdditive (μ i) (T i) (C i)),
  (∀ i ∈ s, MeasureTheory.Integrable f (μ i)) →
    MeasureTheory.setToFun (∑ i ∈ s, μ i) (∑ i ∈ s, T i) ⋯ f = ∑ i ∈ s, MeasureTheory.setToFun (μ i) (T i) ⋯ f
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.isInducing : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → Continuous f → Topology.IsInducing f
-- Mathlib.Logic.Equiv.Defs
Equiv.ofUnique_apply : ∀ (α : Sort u) (β : Sort v) [inst : Unique α] [inst_1 : Unique β] (a : α), (Equiv.ofUnique α β) a = default a
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.mk_obj : ∀ {V : Type u_1} {W : Type u_2} [inst : Quiver V] [inst_1 : Quiver W] {obj : V → W}
  {map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)} {X : V}, { obj := obj, map := map }.obj X = obj X
-- Mathlib.Order.ScottContinuity
ScottContinuous.id : ∀ {α : Type u_1} [inst : Preorder α], ScottContinuous id
-- Init.Prelude
/-- Bitvectors have decidable equality.

This should be used via the instance `DecidableEq (BitVec w)`.
 -/
BitVec.decEq : {w : ℕ} → (x y : BitVec w) → Decidable (x = y)
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenex.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (x : ℕ)
  (h_1 : (x : ℕ) → motive x FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (x : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (x l : ℕ) →
      (R : L.Relations l) → (ts : Fin l → L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (x : ℕ) → (f₁ f₂ : L.BoundedFormula α x) → motive x (f₁.imp f₂))
  (h_5 : (x : ℕ) → (f : L.BoundedFormula α (x + 1)) → motive x f.all),
  (match x, FirstOrder.Language.BoundedFormula.falsum with
    | x, FirstOrder.Language.BoundedFormula.falsum => h_1 x
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 x t₁ t₂
    | x, FirstOrder.Language.BoundedFormula.rel R ts => h_3 x l R ts
    | x, f₁.imp f₂ => h_4 x f₁ f₂
    | x, f.all => h_5 x f) =
    h_1 x
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.IsSimple.isAtom_iff_eq_top : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSimple R L] (I : LieIdeal R L), IsAtom I ↔ I = ⊤
-- Init.Data.List.Sublist
List.suffix_append_self_iff : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁ ++ l₃ <:+ l₂ ++ l₃ ↔ l₁ <:+ l₂
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- This is the functor `F ↦ X ↦ YonedaCollection F X`.  -/
CategoryTheory.OverPresheafAux.yonedaCollectionFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      CategoryTheory.Functor
        (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v))
        (CategoryTheory.Functor Cᵒᵖ (Type v))
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Pos.Raw.get?.match_1.splitter : (motive : String → String.Pos.Raw → Sort u_1) →
  (x : String) → (x_1 : String.Pos.Raw) → ((s : String) → (p : String.Pos.Raw) → motive s p) → motive x x_1
-- Mathlib.Data.Set.Finite.Basic
Set.infinite_image_iff : ∀ {α : Type u} {β : Type v} {s : Set α} {f : α → β}, Set.InjOn f s → ((f '' s).Infinite ↔ s.Infinite)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.abs_abv_sub_le_abv_sub : ∀ {R : Type u_5} {S : Type u_6} [inst : Ring R] [inst_1 : CommRing S] [inst_2 : LinearOrder S] [IsStrictOrderedRing S]
  (abv : AbsoluteValue R S) (a b : R), |abv a - abv b| ≤ abv (a - b)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lift_lt : ∀ {a b : Ordinal.{v}}, Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} b ↔ a < b
-- Mathlib.NumberTheory.NumberField.Basic
/-- The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 -/
NumberField.term𝓞 : Lean.ParserDescr