mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Expr.toPoly.go.match_1.eq_2 : ∀ (motive : Nat.Internal.Linear.Expr → Sort u_1) (i : Nat.Internal.Linear.Var)
  (h_1 : (k : ℕ) → motive (Nat.Internal.Linear.Expr.num k))
  (h_2 : (i : Nat.Internal.Linear.Var) → motive (Nat.Internal.Linear.Expr.var i))
  (h_3 : (a b : Nat.Internal.Linear.Expr) → motive (a.add b))
  (h_4 : (k : ℕ) → (a : Nat.Internal.Linear.Expr) → motive (Nat.Internal.Linear.Expr.mulL k a))
  (h_5 : (a : Nat.Internal.Linear.Expr) → (k : ℕ) → motive (a.mulR k)),
  (match Nat.Internal.Linear.Expr.var i with
    | Nat.Internal.Linear.Expr.num k => h_1 k
    | Nat.Internal.Linear.Expr.var i => h_2 i
    | a.add b => h_3 a b
    | Nat.Internal.Linear.Expr.mulL k a => h_4 k a
    | a.mulR k => h_5 a k) =
    h_2 i
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.truncGE.rightHomologyMapData_φQ : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] {i j k : ι} {j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i)
  (hk : c.next j = k) (hj : e.BoundaryGE j),
  (HomologicalComplex.truncGE.rightHomologyMapData K e hj' hi hk hj).φQ = (K.truncGE'XIsoOpcycles e hj' hj).inv
-- Mathlib.Topology.Sets.Closeds
/-- Reinterpret a clopen as an open.  -/
TopologicalSpace.Clopens.toOpens : {α : Type u_2} → [inst : TopologicalSpace α] → TopologicalSpace.Clopens α → TopologicalSpace.Opens α
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.instToSnapshotTreeTacticParsedSnapshotInner : {α : Type} →
  [Lean.Language.ToSnapshotTree α] → Lean.Language.ToSnapshotTree (Lean.Elab.Tactic.TacticParsedSnapshotInner α)
-- Init.Grind.Lemmas
Lean.Grind.of_decide_eq_true : ∀ {p : Prop} {x : Decidable p}, decide p = true → p = True
-- Init.PropLemmas
forall_or_imp_or_self_right_left : ∀ {α : Sort u_1} {P Q R : α → Prop}, (∀ (a : α), P a ∨ Q a → Q a ∨ R a) ↔ ∀ (a : α), P a → Q a ∨ R a
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.glueDist_triangle_inl_inr_inl : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [Nonempty Z] (Φ : Z → X)
  (Ψ : Z → Y) (ε : ℝ),
  (∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε) →
    ∀ (x : X) (y : Y) (z : X),
      Metric.glueDist Φ Ψ ε (Sum.inl x) (Sum.inl z) ≤
        Metric.glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + Metric.glueDist Φ Ψ ε (Sum.inr y) (Sum.inl z)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.imports : Lean.ParseImports.State → Array Lean.Import
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ΨSq_three : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.ΨSq 3 = W.Ψ₃ ^ 2
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pos_iff_pos_of_mul_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [PosMulReflectLT α] [MulPosReflectLT α],
  0 < a * b → (0 < a ↔ 0 < b)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_map_eq_toList_mapM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → γ} {it : Std.IterM m β},
  (Std.IterM.map f it).toList = (Std.IterM.mapM (fun b => pure (f b)) it).toList
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
/-- The morphism `M.exteriorPower n ⟶ N` induced by an alternating map.  -/
ModuleCat.exteriorPower.desc : {R : Type u} →
  [inst : CommRing R] → {M : ModuleCat R} → {n : ℕ} → {N : ModuleCat R} → M.AlternatingMap N n → (M.exteriorPower n ⟶ N)
-- Mathlib.Topology.Sets.OpenCover
TopologicalSpace.IsOpenCover.exists_finite_of_compactSpace : ∀ {ι : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] {u : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover u → ∀ [CompactSpace X], ∃ s, TopologicalSpace.IsOpenCover fun i => u ↑i
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_range_succ : ∀ {α : Type u_1} {Ω : Type u_2} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : CommMonoid β] [MeasurableMul₂ β]
  {f : ℕ → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ℕ), Measurable (f i)) → ∀ (n : ℕ), ProbabilityTheory.Kernel.IndepFun (∏ j ∈ Finset.range n, f j) (f n) κ μ
-- Mathlib.Data.Finset.Sups
Finset.diffs_inter_subset_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s₁ s₂ t : Finset α},
  (s₁ ∩ s₂).diffs t ⊆ s₁.diffs t ∩ s₂.diffs t
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stepAux.match_1.eq_4 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ]
  (motive : Turing.TM1.Stmt Γ Λ σ → σ → Turing.Tape Γ → Sort u_4) (p : Γ → σ → Bool) (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ)
  (v : σ) (T : Turing.Tape Γ)
  (h_1 :
    (d : Turing.Dir) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.move d q) v T)
  (h_2 :
    (a : Γ → σ → Γ) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.write a q) v T)
  (h_3 :
    (s : Γ → σ → σ) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.load s q) v T)
  (h_4 :
    (p : Γ → σ → Bool) →
      (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v T)
  (h_5 : (l : Γ → σ → Λ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.goto l) v T)
  (h_6 : (v : σ) → (T : Turing.Tape Γ) → motive Turing.TM1.Stmt.halt v T),
  (match Turing.TM1.Stmt.branch p q₁ q₂, v, T with
    | Turing.TM1.Stmt.move d q, v, T => h_1 d q v T
    | Turing.TM1.Stmt.write a q, v, T => h_2 a q v T
    | Turing.TM1.Stmt.load s q, v, T => h_3 s q v T
    | Turing.TM1.Stmt.branch p q₁ q₂, v, T => h_4 p q₁ q₂ v T
    | Turing.TM1.Stmt.goto l, v, T => h_5 l v T
    | Turing.TM1.Stmt.halt, v, T => h_6 v T) =
    h_4 p q₁ q₂ v T
-- Mathlib.MeasureTheory.Measure.Restrict
piecewise_ae_eq_of_ae_eq_set : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} {f g : α → β}
  [inst_1 : DecidablePred fun x => x ∈ s] [inst_2 : DecidablePred fun x => x ∈ t],
  s =ᵐ[μ] t → s.piecewise f g =ᵐ[μ] t.piecewise f g
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- Build a `BialgEquiv` from an isomorphism in the category `CommHopfAlgCat R`.  -/
CommHopfAlgCat.ofIso : {R : Type u} → [inst : CommRing R] → {A B : CommHopfAlgCat R} → (A ≅ B) → ↑A ≃ₐc[R] ↑B
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- Constructor for composition  -/
PFunctor.comp.mk : (P₂ : PFunctor.{uA₂, uB₂}) → (P₁ : PFunctor.{uA₁, uB₁}) → {α : Type v} → ↑P₂ (↑P₁ α) → ↑(P₂.comp P₁) α
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_toAlgHom_injective : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂], Function.Injective AlgEquiv.toAlgHom
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.ext_iff : ∀ {R : Type u} {a b : R} {x y : QuadraticAlgebra R a b}, x = y ↔ x.re = y.re ∧ x.im = y.im
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.red_iff_irreducible : ∀ {α : Type u} {L : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool},
  (x1, b1) ≠ (x2, b2) → (FreeGroup.Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)])
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- If `h : IsZero X`, then `h.to_ Y` is a choice of unique morphism `X → Y`.

`to` is a reserved word, it was replaced by `to_`
 -/
CategoryTheory.Limits.IsZero.to_ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X : C} → CategoryTheory.Limits.IsZero X → (Y : C) → X ⟶ Y
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Notation for an oplax functor between bicategories.  -/
CategoryTheory.Bicategory.«term_⥤ᵒᵖᴸ_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Localization.FractionRing
instIsFractionRing : ∀ {R : Type u_6} [inst : Field R], IsFractionRing R R
-- Mathlib.Order.Heyting.Basic
PUnit.hnot_eq : ∀ (a : PUnit.{u + 1}), ￢a = PUnit.unit
-- Mathlib.Analysis.Seminorm
/-- `Seminorm 𝕜 E` is a conditionally complete lattice.

Note that, while `inf`, `sup` and `sSup` have good definitional properties (corresponding to
the instances given here for `Inf`, `Sup` and `SupSet` respectively), `sInf s` is just
defined as the supremum of the lower bounds of `s`, which is not really useful in practice. If you
need to use `sInf` on seminorms, then you should probably provide a more workable definition first,
but this is unlikely to happen so we keep the "bad" definition for now.  -/
Seminorm.instConditionallyCompleteLattice : {𝕜 : Type u_3} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] → [inst_2 : Module 𝕜 E] → ConditionallyCompleteLattice (Seminorm 𝕜 E)
-- Mathlib.Algebra.Group.Defs
zpow_neg_one : ∀ {G : Type u_1} [inst : DivInvMonoid G] (x : G), x ^ (-1) = x⁻¹
-- Mathlib.RingTheory.Polynomial.IsIntegral
/-- **Alias** of `IsIntegral.coeff`.

---

[Stacks Tag 00H0](https://stacks.math.columbia.edu/tag/00H0) ((2)) -/
IsIntegral.coeff_of_exists_smul_mem_lifts : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Polynomial S},
  IsIntegral (Polynomial R) p → ∀ (i : ℕ), IsIntegral R (p.coeff i)
-- Mathlib.Order.Basic
Subtype.coe_lt_coe : ∀ {α : Type u_2} [inst : LT α] {p : α → Prop} {x y : Subtype p}, ↑x < ↑y ↔ x < y
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.arrow_iso_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso]
  {f g : CategoryTheory.Arrow C} (e : f ≅ g), P f.hom ↔ P g.hom
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_zero' : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] {ι : Type u_7}
  [Finite ι] [Nonempty ι] (b : Module.Basis ι A M), LinearMap.det 0 = 0
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.map_right_cancel : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {x y : M} {c : ↥S}, f (↑c + x) = f (↑c + y) → f x = f y
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.coe_invFun : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ), φ.invFun = ⇑φ.toLinearEquiv.symm
-- Init.Data.UInt.Bitwise
UInt32.or_neg_one : ∀ {a : UInt32}, a ||| -1 = -1
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_coe_equiv : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S), RingHom.ker ↑f = ⊥
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformlyOn.comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] {γ : Type u_4} [inst_3 : TopologicalSpace γ] {t : Set γ},
  MultipliableLocallyUniformlyOn f s →
    ∀ (h' : γ → β), Set.MapsTo h' t s → ContinuousOn h' t → MultipliableLocallyUniformlyOn (fun i y => f i (h' y)) t
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.induction_on : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  {motive : Matrix.ProjGenLinGroup n R → Prop} (g : Matrix.ProjGenLinGroup n R),
  (∀ (g : GL n R), motive (Matrix.ProjGenLinGroup.mk g)) → motive g
-- Mathlib.CategoryTheory.Limits.Final
/-- When `F` is final, and `F ⋙ G` has a colimit, then `G` has a colimit also.

We can't make this an instance, because `F` is not determined by the goal.
(Even if this weren't a problem, it would cause a loop with `comp_hasColimit`.)
 -/
CategoryTheory.Functor.Final.hasColimit_of_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} [CategoryTheory.Limits.HasColimit (F.comp G)], CategoryTheory.Limits.HasColimit G
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : Colex α) (b : β), ofColex (a ^ b) = ofColex a ^ b
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.on_subset : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α}
  {t : Set α}, IsLocalMinOn f t a → s ⊆ t → IsLocalMinOn f s a
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↥U),
  hU.primeIdealOf x =
    (AlgebraicGeometry.Spec.map (X.presheaf.germ U ↑x ⋯)) (IsLocalRing.closedPoint ↑(X.presheaf.stalk ↑x))
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_eq_push : ∀ {m n : ℤ}, m + 1 < n → (m<...n).toArray = (m<...n - 1).toArray.push (n - 1)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.CliqueFree.card_edgeFinset_le : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ},
  G.CliqueFree (r + 1) →
    have n := Fintype.card V;
    G.edgeFinset.card ≤ (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
SeminormedAddCommGroup.toPseudoMetricSpace.hcongr_2 : ∀ (E E' : Type u_8),
  E = E' →
    ∀ (self : SeminormedAddCommGroup E) (self' : SeminormedAddCommGroup E'),
      self ≍ self' → self.toPseudoMetricSpace ≍ self'.toPseudoMetricSpace
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.instReprSplitStatus : Repr Lean.Meta.Grind.SplitStatus
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfpFamily.eq_1 : ∀ {ι : Type u_1} (f : ι → Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}), Ordinal.nfpFamily f a = ⨆ i, List.foldr f a i
-- Init.Data.SInt.Lemmas
Int8.toUInt8_ofBitVec : ∀ (b : BitVec 8), (Int8.ofBitVec b).toUInt8 = { toBitVec := b }
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.case_eval : ∀ (f g : Turing.ToPartrec.Code),
  (f.case g).eval = fun v => Nat.rec (f.eval v.tail) (fun y x => g.eval (y :: v.tail)) v.headI
-- Mathlib.Computability.Partrec
Computable.vector_ofFn' : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Computable List.Vector.ofFn
-- Mathlib.Analysis.Complex.Circle
Circle.instSMulCommClass_right : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul ℂ β] [inst_1 : SMul α β] [SMulCommClass α ℂ β], SMulCommClass α Circle β
-- Init.Data.List.MapIdx
List.mapIdx.go.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (f : ℕ → α → β) (a : Array β) (a_1 : α) (as : List α),
  List.mapIdx.go f (a_1 :: as) a = List.mapIdx.go f as (a.push (f a.size a_1))
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- For `0 ≤ x`, the only problematic case in the equality `x ^ y * x ^ z = x ^ (y + z)` is for
`x = 0` and `y + z = 0`, where the right-hand side is `1` while the left-hand side can vanish.
The inequality is always true, though, and given in this lemma.  -/
Real.le_rpow_add : ∀ {x : ℝ}, 0 ≤ x → ∀ (y z : ℝ), x ^ y * x ^ z ≤ x ^ (y + z)
-- Mathlib.Control.Functor.Multivariate
_private.Mathlib.Control.Functor.Multivariate.0.MvFunctor.f' : {β : Type u} →
  (rr : β → β → Prop) →
    (n : ℕ) →
      (α : TypeVec.{u} n) →
        TypeVec.Arrow (fun i => { p_1 // TypeVec.ofRepeat (α.RelLast' rr i (TypeVec.prod.mk i p_1.1 p_1.2)) }) fun i =>
          { p_1 // α.RelLast rr p_1.1 p_1.2 }
-- Mathlib.Data.List.Sigma
List.lookupAll.congr_simp : ∀ {α : Type u} {β : α → Type v} {inst : DecidableEq α} [inst_1 : DecidableEq α] (a : α) (a_1 a_2 : List (Sigma β)),
  a_1 = a_2 → List.lookupAll a a_1 = List.lookupAll a a_2
-- Init.Data.UInt.Lemmas
USize.neg_one_eq : -1 = USize.ofNatLT (USize.size - 1) ⋯
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.replicateAddMonoidHom_apply : ∀ {α : Type u_1} (a : α) (n : ℕ), (Multiset.replicateAddMonoidHom a) n = Multiset.replicate n a
-- Mathlib.Algebra.Group.Hom.Defs
/-- Turn an element of a type `F` satisfying `OneHomClass F M N` into an actual
`OneHom`. This is declared as the default coercion from `F` to `OneHom M N`.  -/
OneHomClass.toOneHom : {M : Type u_4} →
  {N : Type u_5} →
    {F : Type u_9} → [inst : One M] → [inst_1 : One N] → [inst_2 : FunLike F M N] → [OneHomClass F M N] → F → OneHom M N
-- Mathlib.MeasureTheory.Measure.Regular
/-- **Alias** of `MeasurableSet.exists_isOpen_sdiff_lt`. -/
MeasurableSet.exists_isOpen_diff_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [μ.OuterRegular]
  {A : Set α}, MeasurableSet A → μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ U ⊇ A, IsOpen U ∧ μ U < ⊤ ∧ μ (U \ A) < ε
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.notMem_closure_iff : ∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α},
  M.Indep I →
    autoParam (e ∈ M.E) Matroid.Indep.notMem_closure_iff._auto_1 → (e ∉ M.closure I ↔ M.Indep (insert e I) ∧ e ∉ I)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_roo_eq_none : ∀ {m n i : ℕ}, n ≤ i + (m + 1) → (m<...n).toArray[i]? = none
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimit_iff_isSuccLimit : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [NoMinOrder α], Order.IsSuccPrelimit a ↔ Order.IsSuccLimit a
-- Mathlib.RingTheory.Idempotents
instRingCorner : {R : Type u_1} → (e : R) → [inst : NonUnitalRing R] → (idem : IsIdempotentElem e) → Ring idem.Corner
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_comap_le : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup N),
  AddSubgroup.map f (AddSubgroup.comap f H) ≤ H
-- Init.Data.List.Nat.Count
_private.Init.Data.List.Nat.Count.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.Data.Num.Bitwise
instInhabitedSNum : Inhabited SNum
-- Mathlib.CategoryTheory.Filtered.Flat
CategoryTheory.isFiltered_of_representablyCoflat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsFiltered D] [CategoryTheory.RepresentablyCoflat F],
  CategoryTheory.IsFiltered C
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which monovary together, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not monovary together. Stated by permuting the entries of `g`.  -/
Monovary.sum_smul_comp_perm_lt_sum_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Monovary f g → (∑ i, f i • g (σ i) < ∑ i, f i • g i ↔ ¬Monovary f (g ∘ ⇑σ))
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
add_neg_lt_iff_le_add' : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, a + -b < c ↔ a < b + c
-- Mathlib.Topology.Category.Born
Born.instConcreteCategoryLocallyBoundedMapCarrier : CategoryTheory.ConcreteCategory Born fun x1 x2 => LocallyBoundedMap x1.carrier x2.carrier
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS'_one : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ), complEDS' b c d k 1 = 1
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.map_mono : ∀ {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 : L →ₗ⁅R⁆ L'}, Monotone (LieIdeal.map f)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)], k ∉ t₂ → (t₁ \ t₂).get! k = t₁.get! k
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The isomorphism between the quotient of a product by the image of the multiplication-by-`n`
map and the product of the quotients by the images of the multiplication-by-`n` maps
on the factors.  -/
QuotientAddGroup.addEquivPiModRangeNSMulAddMonoidHom : {ι : Type u_1} →
  (A : ι → Type u_2) →
    [inst : (i : ι) → AddCommGroup (A i)] →
      (n : ℕ) → ((i : ι) → A i) ⧸ (nsmulAddMonoidHom n).range ≃+ ((i : ι) → A i ⧸ (nsmulAddMonoidHom n).range)
-- Lean.Meta.Tactic.Grind.EMatch
/-- Helper function for testing constraints of the form `is_value e` and `is_strict_value e`  -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.isValue : Lean.Expr → Bool → Lean.MetaM Bool
-- Mathlib.Order.Filter.CountableInter
/-- **Alias** of `Filter.EventuallyEq.countable_bUnion`. -/
EventuallyEq.countable_bUnion : ∀ {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι},
  S.Countable →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) → ⋃ i, ⋃ (h : i ∈ S), s i h =ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} {fallback : β a}, a ∉ m → m.getD a fallback = fallback
-- Mathlib.Order.WithBot
WithTop.some_eq_map_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {y : β} {v : WithTop α}, ↑y = WithTop.map f v ↔ ∃ x, v = ↑x ∧ f x = y
-- Init.Data.Int.Lemmas
Int.add_neg_cancel_right : ∀ (a b : ℤ), a + b + -b = a
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableDiv₂.mk : ∀ {G₀ : Type u_2} [inst : MeasurableSpace G₀] [inst_1 : Div G₀], (Measurable fun p => p.1 / p.2) → MeasurableDiv₂ G₀
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ShowDocumentClientCapabilities.mk : Bool → Lean.Lsp.ShowDocumentClientCapabilities
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonNatTrans_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [inst_5 : F'.LaxMonoidal] (f : F ⟶ F')
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal f] (X : CategoryTheory.Mon C),
  ((CategoryTheory.Functor.mapMonNatTrans f).app X).hom = f.app X.X
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.instMonoidWithZeroHomClassReal : ∀ {K : Type u_1} [inst : Field K], MonoidWithZeroHomClass (NumberField.InfinitePlace K) K ℝ
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.ext : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  {f₁ f₂ : 𝒜 →ₐᵍ[R] ℬ}, (∀ (x : A), f₁ x = f₂ x) → f₁ = f₂
-- Init.Data.SInt.Lemmas
ISize.add_zero : ∀ (a : ISize), a + 0 = a
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addZeroClass : {α : Type u} → [AddZeroClass α] → AddZeroClass (WithTop α)
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- The Gromov-Hausdorff space is complete.  -/
GromovHausdorff.instCompleteSpaceGHSpace : CompleteSpace GromovHausdorff.GHSpace