mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Basic
/-- If `M` is a topological module over `R` and `0` is a limit of invertible elements of `R`, then
`⊤` is the only submodule of `M` with a nonempty interior.
This is the case, e.g., if `R` is a nontrivially normed field.  -/
Submodule.eq_top_of_nonempty_interior' : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] [ContinuousAdd M] [inst_5 : Module R M] [ContinuousSMul R M]
  [(nhdsWithin 0 {x | IsUnit x}).NeBot] (s : Submodule R M), (interior ↑s).Nonempty → s = ⊤
-- Mathlib.Data.Int.Fib.Basic
Int.fib_eq_fib_add_two_sub_fib_add_one : ∀ (n : ℤ), Int.fib n = Int.fib (n + 2) - Int.fib (n + 1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k : α}, k ∉ m₂ → (m₁ ∩ m₂).getKey! k = default
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuous_div_const : ∀ (c : ENNReal), c ≠ 0 → Continuous fun x => x / c
-- Mathlib.Algebra.Category.Ring.FilteredColimits
SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_quotMk : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J SemiRingCat}
  [inst_1 : CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) {j : J} (x : ↑(F.obj j)),
  (SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom t)
      (Quot.mk ((F.comp (CategoryTheory.forget₂ SemiRingCat MonCat)).comp (CategoryTheory.forget MonCat)).ColimitTypeRel
        ⟨j, x⟩) =
    (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) x
-- Mathlib.Algebra.Algebra.Unitization
Unitization.linearMap_ext_iff : ∀ {S : Type u_2} {R : Type u_3} {A : Type u_4} {N : Type u_5} [inst : CommSemiring S] [inst_1 : AddCommMonoid R]
  [inst_2 : AddCommMonoid A] [inst_3 : AddCommMonoid N] [inst_4 : Module S R] [inst_5 : Module S A]
  [inst_6 : Module S N] {f g : Unitization R A →ₗ[S] N},
  f = g ↔ (∀ (r : R), f (Unitization.inl r) = g (Unitization.inl r)) ∧ ∀ (a : A), f ↑a = g ↑a
-- Batteries.Data.Char.Basic
Char.any_eq_true_iff_exists_eq_true : ∀ {p : Char → Bool}, Char.any p = true ↔ ∃ c, p c = true
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.instIsDenseSubsiteInducedTopologyInverseFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D),
  CategoryTheory.Functor.IsDenseSubsite J (e.inverse.inducedTopology J) e.functor
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instFiniteMap : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finite] {f : α → β} (hf : Set.InjOn f M.E), (M.map f hf).Finite
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Seq.unionFuel.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (fuel : ℕ) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ),
  (match fuel.succ with
    | 0 => h_1 ()
    | fuel.succ => h_2 fuel) =
    h_2 fuel
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.lift_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (f : F' ⟶ F)
  {G : CategoryTheory.Subfunctor F} (hf : CategoryTheory.Subfunctor.range f ≤ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.lift f hf) G.ι = f
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.mem_toNonUnitalStarSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] {s : NonUnitalSubalgebra R A} {h_star : ∀ x ∈ s, star x ∈ s} {x : A},
  x ∈ s.toNonUnitalStarSubalgebra h_star ↔ x ∈ s
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
IntermediateField.isAlgebraic_adjoin_iff : ∀ {F : Type u_2} {E : Type u_3} {S : Type u_5} {s : Set E} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Ring S] [inst_4 : Algebra E S] {x : S},
  IsAlgebraic (↥(IntermediateField.adjoin F s)) x ↔ IsAlgebraic (↥(Algebra.adjoin F s)) x
-- Mathlib.LinearAlgebra.TensorPower.Pairing
TensorPower.multilinearMapToDual_apply_tprod : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (f : Fin n → Module.Dual R M) (v : Fin n → M),
  ((TensorPower.multilinearMapToDual R M n) f) ((PiTensorProduct.tprod R) v) = ∏ i, (f i) (v i)
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.overrideCasesOn : Lean.Elab.ComputedFields.M Unit
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.delabFor : Lean.Name → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick
/-- Joyal's trick (dual): that trivial cofibrations have the left lifting
property with respect to fibrations follows from the left lifting property
of cofibrations with respect to trivial fibrations and a few other
consequences of the model categories axioms.  -/
HomotopicalAlgebra.ModelCategory.hasLiftingProperty_of_joyalTrickDual : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : HomotopicalAlgebra.CategoryWithFibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty]
  [(HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C)]
  [CategoryTheory.Limits.HasPullbacks C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition]
  [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange],
  (∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.WeakEquivalence p]
      [HomotopicalAlgebra.Fibration p], CategoryTheory.HasLiftingProperty i p) →
    ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.Fibration p]
      [HomotopicalAlgebra.WeakEquivalence i], CategoryTheory.HasLiftingProperty i p
-- Mathlib.Analysis.InnerProductSpace.Coalgebra
/-- The counit on `n → 𝕜` corresponds to the Euclidean space adjoint of the algebra linear map.  -/
Pi.counit_eq_adjoint : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_3} [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  CoalgebraStruct.counit =
    LinearMap.adjoint (↑↑(EuclideanSpace.equiv n 𝕜).symm ∘ₗ Algebra.linearMap 𝕜 (n → 𝕜)) ∘ₗ
      ↑↑(EuclideanSpace.equiv n 𝕜).symm
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.remainingBytes.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.remainingBytes = s.rawEndPos.byteIdx - i.byteIdx
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffAt.clm_precomp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₁ →L[𝕜] F₂}
  {x : M},
  ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n f x →
    ContMDiffAt I (modelWithCornersSelf 𝕜 ((F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃)) n
      (fun y => ContinuousLinearMap.precomp F₃ (f y)) x
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.floor_add_sum : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] {f : (ι → ℕ) → ℕ} {x : ι → ℕ}
  {i : ↑(IsProperLinearSet.basisSet✝ hs)},
  IsProperLinearSet.floor✝ hs (x + ∑ j, f ↑j • ↑j) i = IsProperLinearSet.floor✝ hs x i + ↑(f ↑i)
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_succ' : ∀ (i : ℕ) {n m : ℕ} (h : autoParam (n + (i + 1) = m) SimplexCategory.δ₀Iter_succ'._auto_1),
  SimplexCategory.δ₀Iter (i + 1) h =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ 0) (SimplexCategory.δ₀Iter i ⋯)
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
ModularForm.levelOne_weight_four_rank_one : Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 4) = 1
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.mulLeft_mul` for matrix multiplication.  -/
mulLeftLinearMap_mul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} {A : Type u_6} [inst : Fintype m]
  [inst_1 : Fintype n] [inst_2 : Semiring R] [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A]
  [inst_5 : SMulCommClass R A A] (a : Matrix l m A) (b : Matrix m n A),
  mulLeftLinearMap o R (a * b) = mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.instTransZigzag : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    Trans (fun x1 x2 => CategoryTheory.Zigzag x1 x2) (fun x1 x2 => CategoryTheory.Zigzag x1 x2) fun x1 x2 =>
      CategoryTheory.Zigzag x1 x2
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.PreSubmersivePresentation.ofHasCoeffs_val : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] (P : Algebra.PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀] (i : ι),
  (P.ofHasCoeffs R₀).val i =
    (Ideal.Quotient.mk (Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀)))) (MvPolynomial.X i)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.le_one_iff_le_one : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {x : R}, v₁ x ≤ 1 ↔ v₂ x ≤ 1
-- Mathlib.RingTheory.Polynomial.Basic
MvPolynomial.renameEquiv.eq_1 : ∀ {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [inst : CommSemiring R] (f : σ ≃ τ),
  MvPolynomial.renameEquiv R f =
    { toFun := ⇑(MvPolynomial.rename ⇑f), invFun := ⇑(MvPolynomial.rename ⇑f.symm), left_inv := ⋯, right_inv := ⋯,
      map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.leftToRight_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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful]
  {X : C},
  t.leftToRight.app X =
    CategoryTheory.CategoryStruct.comp (t.adj₂.unit.app (F.obj X)) (CategoryTheory.inv (H.map (t.adj₁.unit.app X)))
-- Mathlib.Order.CompleteLattice.Basic
iInf₂_le : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α] {f : (i : ι) → κ i → α} (i : ι) (j : κ i),
  ⨅ i, ⨅ j, f i j ≤ f i j
-- Mathlib.Control.Functor.Multivariate
/-- relational lifting over multivariate functors  -/
MvFunctor.LiftR : {n : ℕ} →
  {F : TypeVec.{u} n → Type v} →
    [MvFunctor F] → {α : TypeVec.{u} n} → (⦃i : Fin2 n⦄ → α i → α i → Prop) → F α → F α → Prop
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
/-- `μ` is the Möbius function. If `n` is squarefree with an even number of distinct prime factors,
`μ n = 1`. If `n` is squarefree with an odd number of distinct prime factors, `μ n = -1`.
If `n` is not squarefree, `μ n = 0`.  -/
ArithmeticFunction.Moebius.termμ : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
LipschitzWith.compLp.congr_simp : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {g g_1 : E → F} (e_g : g = g_1) {c c_1 : NNReal}
  (e_c : c = c_1) (hg : LipschitzWith c g) (g0 : g 0 = 0) (f f_1 : ↥(MeasureTheory.Lp E p μ)),
  f = f_1 → hg.compLp g0 f = ⋯.compLp ⋯ f_1
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderivWithin_sumInl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {p : M ⊕ M'} {q : M},
  UniqueMDiffAt[s] q → mfderiv[s] Sum.inl q = ContinuousLinearMap.id 𝕜 (TangentSpace I p)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.norm_compMeasurePreserving : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β} {f : α → β}
  (g : ↥(MeasureTheory.Lp E p μb)) (hf : MeasureTheory.MeasurePreserving f μ μb),
  ‖(MeasureTheory.Lp.compMeasurePreserving f hf) g‖ = ‖g‖
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_of_perm : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Inhabited β] {l l' : List ((_ : α) × β)}
  {a : α},
  Std.Internal.List.DistinctKeys l → l.Perm l' → Std.Internal.List.getValue! a l = Std.Internal.List.getValue! a l'
-- Mathlib.Analysis.Convex.Visible
IsVisible.eq_1 : ∀ (𝕜 : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : AddCommGroup V]
  [inst_3 : Module 𝕜 V] [inst_4 : AddTorsor V P] (s : Set P) (x y : P),
  IsVisible 𝕜 s x y = ∀ ⦃z : P⦄, z ∈ s → ¬Sbtw 𝕜 x z y
-- Mathlib.Data.Finsupp.ToDFinsupp
Finsupp.toDFinsupp_toFinsupp : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : ι →₀ M), f.toDFinsupp.toFinsupp = f
-- Mathlib.Order.Interval.Set.Monotone
StrictMonoOn.Iic_id_le : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] [OrderBot α] {n : α} {φ : α → α},
  StrictMonoOn φ (Set.Iic n) → ∀ m ≤ n, m ≤ φ m
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_eq_of_not_mem : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {m : ℕ} {x : A},
  x ∉ I → DividedPowers.OfInvertibleFactorial.dpow I m x = 0
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.liftSemilatticeSup.eq_1 : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder β] [inst_1 : SemilatticeSup α]
  (gi : GaloisInsertion l u),
  gi.liftSemilatticeSup =
    { toPartialOrder := inst, sup := fun a b => l (u a ⊔ u b), le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the sign of the angle between two vectors is positive, the second vector is nonzero.  -/
Orientation.right_ne_zero_of_oangle_sign_eq_one : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, (o.oangle x y).sign = 1 → y ≠ 0
-- Mathlib.Util.Export
Lean.Export.Entry.name.sizeOf_spec : ∀ (n : Lean.Name), sizeOf (Lean.Export.Entry.name n) = 1 + sizeOf n
-- Init.Data.BitVec.Basic
/-- Unsigned division of bitvectors using the Lean convention where division by zero returns zero.
Usually accessed via the `/` operator.
 -/
BitVec.udiv : {n : ℕ} → BitVec n → BitVec n → BitVec n
-- Mathlib.Data.DFinsupp.WellFounded
Pi.Colex.wellFoundedLT : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [Finite ι] [inst_2 : (i : ι) → LT (α i)]
  [∀ (i : ι), WellFoundedLT (α i)], WellFoundedLT (Colex ((i : ι) → α i))
-- Std.Data.TreeMap.Lemmas
/-- Simpler variant of `getD_filter` when `LawfulEqCmp` is available.  -/
Std.TreeMap.getD_filter' : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {f : α → β → Bool} {k : α} {fallback : β},
  (Std.TreeMap.filter f t).getD k fallback = (Option.filter (f k) t[k]?).getD fallback
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_eq_bot : ∀ {R : Type u_2} [inst : NonAssocSemiring R] {S : Subsemiring Rᵐᵒᵖ}, S.unop = ⊥ ↔ S = ⊥
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instZero.eq_1 : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β],
  BoundedContinuousFunction.instZero = { zero := BoundedContinuousFunction.const α 0 }
-- Init.Data.Int.Linear
Int.Internal.Linear.instBEqPoly.beq_spec_3 : ∀ (x x_1 : Int.Internal.Linear.Poly),
  (∀ (a b : ℤ), x = Int.Internal.Linear.Poly.num a → x_1 = Int.Internal.Linear.Poly.num b → False) →
    (∀ (a : ℤ) (a_1 : Int.Internal.Linear.Var) (a_2 : Int.Internal.Linear.Poly) (b : ℤ) (b_1 : Int.Internal.Linear.Var)
        (b_2 : Int.Internal.Linear.Poly),
        x = Int.Internal.Linear.Poly.add a a_1 a_2 → x_1 = Int.Internal.Linear.Poly.add b b_1 b_2 → False) →
      (x == x_1) = false
-- Mathlib.Data.FunLike.IsApply
IsIntCastApply.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} [inst : FunLike F α α] [inst_1 : IntCast F] [inst_2 : SMul ℤ α],
  (∀ (n : ℤ) (x : α), ↑n x = n • x) → IsIntCastApply F α
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the angle between two vectors is `π`, the vectors are not equal.  -/
Orientation.ne_of_oangle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑Real.pi → x ≠ y
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- **Alias** of `Subgroup.normal_of_isMulCommutative`. -/
Subgroup.normal_of_comm : ∀ {G : Type u_1} [inst : Group G] [IsMulCommutative G] (H : Subgroup G), H.Normal
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- `Fintype` for `neighborSet`  -/
SimpleGraph.neighborSetFintype : {V : Type u_1} → (G : SimpleGraph V) → [Fintype V] → [DecidableRel G.Adj] → (v : V) → Fintype ↑(G.neighborSet v)
-- Mathlib.Algebra.Ring.CharZero
add_self_eq_zero : ∀ {R : Type u_2} [inst : NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R}, a + a = 0 ↔ a = 0
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.mk : {A : Type u_6} →
  {B : Type u_7} →
    [inst : Monoid A] →
      [inst_1 : Star A] →
        [inst_2 : Monoid B] →
          [inst_3 : Star B] →
            (toMonoidHom : A →* B) →
              (∀ (a : A), (↑toMonoidHom).toFun (star a) = star ((↑toMonoidHom).toFun a)) → A →⋆* B
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.instDecidableRelAdjLabelGraphOfDecidableEq : {V : Type u_1} →
  {G : SimpleGraph V} →
    {K : Type u_3} →
      [DecidableRel G.Adj] → [DecidableEq K] → (k : K) → {C : G.EdgeLabeling K} → DecidableRel (C.labelGraph k).Adj
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- `Fintype.sum_equiv` is a specialization of `Finset.sum_bij` that
automatically fills in most arguments.

See `Equiv.sum_comp` for a version without `h`.  -/
Fintype.sum_equiv : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid M]
  (e : ι ≃ κ) (f : ι → M) (g : κ → M), (∀ (x : ι), f x = g (e x)) → ∑ x, f x = ∑ x, g x
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.val_signDet_mk : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : Fact (Even (Fintype.card n))] [inst_4 : LinearOrder R] [inst_5 : IsStrictOrderedRing R] (g : GL n R),
  ↑(Matrix.ProjGenLinGroup.signDet (Matrix.ProjGenLinGroup.mk g)) = SignType.sign ↑(Matrix.GeneralLinearGroup.det g)
-- Mathlib.MeasureTheory.Group.Prod
MeasurableEquiv.shearAddRight.eq_1 : ∀ (G : Type u_1) [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : MeasurableAdd₂ G]
  [inst_3 : MeasurableNeg G],
  MeasurableEquiv.shearAddRight G =
    { toEquiv := (Equiv.refl G).prodShear Equiv.addLeft, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Mathlib.Topology.Algebra.Group.Matrix
/-- The natural map from `SL n A` in `GL n A` is an embedding, i.e. it is an injection and
the topology on `SL n A` coincides with the subspace topology from `GL n A`.  -/
Matrix.SpecialLinearGroup.isEmbedding_toGL : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [IsTopologicalRing R], Topology.IsEmbedding ⇑Matrix.SpecialLinearGroup.toGL
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.instContainsZeroIsZeroOfHasZeroObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.ObjectProperty.ContainsZero CategoryTheory.Limits.IsZero
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.coe_of : ∀ (α : Type u_1) [inst : OmegaCompletePartialOrder α], { carrier := α, str := inst }.carrier = α
-- Mathlib.Analysis.Complex.OpenMapping
Complex.isOpenQuotientMap_pow_compl_zero : ∀ (n : ℕ) [NeZero n], IsOpenQuotientMap fun z => ⟨↑z ^ n, ⋯⟩
-- Mathlib.Computability.TuringMachine.Computable
/-- A proof that the identity map on α is computable in time.  -/
Turing.idComputableInTime : {α αΓ : Type} → [Fintype αΓ] → (ea : α → List αΓ) → Turing.TM2ComputableInTime ea ea id
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Stats.mk.sizeOf_spec : ∀ (usedTheorems : Lean.Meta.Simp.UsedSimps) (diag : Lean.Meta.Simp.Diagnostics),
  sizeOf { usedTheorems := usedTheorems, diag := diag } = 1 + sizeOf usedTheorems + sizeOf diag
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.Prepartition.forall_biUnionTagged : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (p : (ι → ℝ) → BoxIntegral.Box ι → Prop) (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J),
  (∀ J ∈ π.biUnionTagged πi, p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Functions.term.eq_1 : ∀ {L : FirstOrder.Language} {n : ℕ} (f : L.Functions n), f.term = FirstOrder.Language.func f FirstOrder.Language.var
-- Std.Async.System
/-- The list of users in the group.
 -/
Std.Async.System.GroupInfo.members : Std.Async.System.GroupInfo → Array String
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- A structure for storing information about a parameter of some declaration, usually within some
telescope. We use this for recording the expressions and index associated to a parameter which was
unused in the remainder of the type.

`m!"{param}"` displays as `[{param.type?.get}] (#{param.idx + 1})` if `type?` is `some _`, and as
`parameter #{param.idx + 1}` as a failsafe if `type?` is `none`. (We always expect `type?` to be
`some _`, but would like a fallback if there are unexpected issues in telescoping.)
 -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.Parameter : Type
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Section.coe_mk : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} (σ : G → E) (hσ : Function.RightInverse σ ⇑S.rightHom),
  ⇑{ toFun := σ, rightInverse_rightHom := hσ } = σ
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.mk.inj : ∀ {α : Type u_1} {β : Type u_2} {inst : MeasurableSpace α} {inst_1 : MeasurableSpace β}
  {toFun : α → MeasureTheory.Measure β} {measurable' : Measurable toFun} {toFun_1 : α → MeasureTheory.Measure β}
  {measurable'_1 : Measurable toFun_1},
  { toFun := toFun, measurable' := measurable' } = { toFun := toFun_1, measurable' := measurable'_1 } → toFun = toFun_1