mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.ext : ∀ {X Y : FinBddDistLat} {f g : X ⟶ Y},
  (∀ (x : ↑X.toDistLat), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The kernel fork `kf` is a limit.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isLimitKf : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    (r r' : ℤ) →
                      (hrr' : r + 1 = r') →
                        (hr : r₀ ≤ r) →
                          (pq' pq'' : κ) →
                            (c r).next pq' = pq'' →
                              (i₀' i₀ i₁ i₂ i₃ : ι) →
                                (hi₀' : i₀' = data.i₀ r' pq' ⋯) →
                                  (hi₀ : i₀ = data.i₀ r pq' ⋯) →
                                    (hi₁ : i₁ = data.i₁ pq') →
                                      (hi₂ : i₂ = data.i₂ pq') →
                                        (hi₃ : i₃ = data.i₃ r pq' ⋯) →
                                          (n₀ n₁ n₂ : ℤ) →
                                            (hn₁' : n₁ = data.deg pq') →
                                              [X.HasSpectralSequence data] →
                                                (hn₁ :
                                                    autoParam (n₀ + 1 = n₁)
                                                      CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isLimitKf._auto_1) →
                                                  (hn₂ :
                                                      autoParam (n₁ + 1 = n₂)
                                                        CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isLimitKf._auto_3) →
                                                    CategoryTheory.Limits.IsLimit
                                                      (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kf
                                                        X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂
                                                        hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Real.measure_ext_Ioo_rat : ∀ {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ],
  (∀ (a b : ℚ), μ (Set.Ioo ↑a ↑b) = ν (Set.Ioo ↑a ↑b)) → μ = ν
-- Mathlib.Algebra.Group.Graph
AddMonoidHom.graph_eq_range_prod : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (f : G →+ H),
  f.graph = ((AddMonoidHom.id G).prod f).range
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTrivAt.eq_1 : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (b : B), Z.localTrivAt b = Z.localTriv (Z.indexAt b)
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Std.Do.PredTrans.pushOption.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_top : ∀ {α : Type u_1} [Nonempty α], ∑' (x : α), ⊤ = ⊤
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.apply_symm_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B) (x : B), e (e.symm x) = x
-- Mathlib.CategoryTheory.Limits.Cones
/-- Given a cone morphism `c ⟶ c'`, construct a cone morphism on the mapped cones functorially.  -/
CategoryTheory.Functor.mapConeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (H : CategoryTheory.Functor C D) →
              {F : CategoryTheory.Functor J C} →
                {c c' : CategoryTheory.Limits.Cone F} → (c ⟶ c') → (H.mapCone c ⟶ H.mapCone c')
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.surjOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  Set.SurjOn (↑e) e.source e.target
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicField.instCharZero : ∀ (n : ℕ) (K : Type w) [inst : Field K] [CharZero K], CharZero (CyclotomicField n K)
-- Mathlib.Algebra.Quaternion
/-- Quaternion conjugate as an `AlgEquiv` to the opposite ring.  -/
Quaternion.starAe : {R : Type u_3} → [inst : CommRing R] → Quaternion R ≃ₐ[R] (Quaternion R)ᵐᵒᵖ
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.Finite.hasFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  CategoryTheory.Limits.HasFiniteColimits (PresheafOfModules R)
-- Mathlib.RingTheory.Nilpotent.Basic
IsNilpotent.isUnit_one_add : ∀ {R : Type u_1} [inst : Ring R] {r : R}, IsNilpotent r → IsUnit (1 + r)
-- Mathlib.Algebra.Ring.Ext
NonAssocRing.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : NonAssocRing R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Mathlib.Topology.Algebra.Monoid
monoidHomOfMemClosureRangeCoe.eq_1 : ∀ {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂] [inst_2 : MulOneClass M₁]
  [inst_3 : MulOneClass M₂] [inst_4 : ContinuousMul M₂] {F : Type u_8} [inst_5 : FunLike F M₁ M₂]
  [inst_6 : MonoidHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun f x => f x)),
  monoidHomOfMemClosureRangeCoe f hf = { toFun := f, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.instInv : {G : Type u_1} → [inst : Add G] → {a : G} → Inv (AddConstEquiv G G a a)
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_lt_castPred_iff : ∀ {n : ℕ} {i j : Fin (n + 1)} {hi : i ≠ Fin.last n} {hj : j ≠ Fin.last n}, i.castPred hi < j.castPred hj ↔ i < j
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffAt.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {ι : Type u_3} {f : ι → E → F} {s : Finset ι} {x : E},
  (∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x) → ContDiffAt 𝕜 n (fun x => ∑ i ∈ s, f i x) x
-- Init.SimpLemmas
ite_cond_congr : ∀ {α : Sort u_1} {b c : Prop} {s : Decidable b} [inst : Decidable c] {x y : α},
  b = c → (if b then x else y) = if c then x else y
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation) The limit cone is a limit. See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.hc : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} →
            (self : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) → CategoryTheory.Limits.IsLimit self.c
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Triangle.sOppSide_affineSpan_pair_point_excenter_singleton : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ → i₂ ≠ i₃ → line[ℝ, t.points i₂, t.points i₃].SOppSide (t.points i₁) (Affine.Simplex.excenter t {i₁})
-- Std.Do.Triple.SpecLemmas
getModify.eq_1 : ∀ {σ : Type u} {m : Type u → Type v} [inst : MonadState σ m] (f : σ → σ), getModify f = modifyGet fun s => (s, f s)
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
WithLp.instProdTopologicalSpace.eq_1 : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  WithLp.instProdTopologicalSpace p α β = TopologicalSpace.induced WithLp.ofLp instTopologicalSpaceProd
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.image_iff : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f : E →ₗ.[R] F} {x : E} {y : F} (hx : x ∈ f.domain),
  y = ↑f ⟨x, hx⟩ ↔ (x, y) ∈ f.graph
-- Mathlib.Data.List.Sym
_private.Mathlib.Data.List.Sym.0.List.sym.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → List α → Sort u_2) →
    (x : ℕ) →
      (x_1 : List α) →
        ((x : List α) → motive 0 x) →
          ((x : ℕ) → (x = 0 → False) → motive x []) →
            ((n : ℕ) → (x : α) → (xs : List α) → motive n.succ (x :: xs)) → motive x x_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_inv_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [inst_6 : CategoryTheory.Category.{v₇, u₇} A₂]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} B₂] [inst_8 : CategoryTheory.Category.{v₉, u₉} C₂]
  {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₁₀)
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ ψ').inv.app X_1).snd.app x =
    CategoryTheory.CategoryStruct.id (ψ'.right.obj (ψ.right.obj (X_1.snd.obj x)))
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.map_natCast`. -/
ENat.map_coe : ∀ {α : Type u_1} (f : ℕ → α) (a : ℕ), ENat.map f ↑a = ↑(f a)
-- Mathlib.Order.Circular
sbtw_iff_not_btw : ∀ {α : Type u_1} [inst : CircularOrder α] {a b c : α}, sbtw a b c ↔ ¬btw c b a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey_alter_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : Option β → Option β},
  m.WF → ∀ {hc : k ∈ Std.DHashMap.Raw.Const.alter m k f}, (Std.DHashMap.Raw.Const.alter m k f).getKey k hc = k
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.isOrtho_polarBilin : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {Q : QuadraticMap R M N} {x y : M},
  (Q.polarBilin x) y = 0 ↔ Q.IsOrtho x y
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The functor `ComposableArrows C n ⥤ ComposableArrows C l` obtained by precomposition with
the functor `Fin.natAddLEFunctor`.  -/
CategoryTheory.ComposableArrows.natAddLEFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n k l : ℕ} →
      k + l ≤ n → CategoryTheory.Functor (CategoryTheory.ComposableArrows C n) (CategoryTheory.ComposableArrows C l)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.realize_toPrenexImp : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n : ℕ} [Nonempty M]
  {φ ψ : L.BoundedFormula α n},
  φ.IsPrenex → ψ.IsPrenex → ∀ {v : α → M} {xs : Fin n → M}, (φ.toPrenexImp ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Constructor for wedges.  -/
CategoryTheory.Limits.Wedge.mk : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          (pt : C) →
            (π : (j : J) → pt ⟶ (F.obj (Opposite.op j)).obj j) →
              (∀ ⦃i j : J⦄ (f : i ⟶ j),
                  CategoryTheory.CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) =
                    CategoryTheory.CategoryStruct.comp (π j) ((F.map f.op).app j)) →
                CategoryTheory.Limits.Wedge F
-- Mathlib.RepresentationTheory.Rep.Res
Rep.liftHomOfSurj.congr_simp : ∀ {k : Type u} [inst : Semiring k] {G : Type v1} {H : Type v2} [inst_1 : Monoid G] [inst_2 : Monoid H] (f : H →* G)
  {X Y : Rep.{u_1, u, v1} k G} (hf : Function.Surjective ⇑f) (f' f'_1 : Rep.res f X ⟶ Rep.res f Y),
  f' = f'_1 → Rep.liftHomOfSurj f hf f' = Rep.liftHomOfSurj f hf f'_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblXYZ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P : Fin 3 → R),
  W'.dblXYZ P = ![W'.dblX P, W'.dblY P, W'.dblZ P]
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Splitting.coe_monoidHom_mk : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} (s : G →* E) (hs : Function.RightInverse ⇑s ⇑S.rightHom),
  ↑{ toMonoidHom := s, rightInverse_rightHom := hs } = s
-- Lean.Meta.Eqns
Lean.Meta.EqnsExtState.mk.inj : ∀ {mapInv mapInv_1 : Lean.PHashMap Lean.Name Lean.Name},
  { mapInv := mapInv } = { mapInv := mapInv_1 } → mapInv = mapInv_1
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.le_ult : ∀ {w : ℕ} (x y : BitVec w), x ≤ y ↔ (!y.ult x) = true
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.not_isFiniteMeasure_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  ¬MeasureTheory.IsFiniteMeasure μ ↔ μ Set.univ = ⊤
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_comp : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] {γ : Type u_4} (f : β → γ),
  MeasureTheory.stoppedProcess (fun t ω => f (u t ω)) τ = fun i ω => f (MeasureTheory.stoppedProcess u τ i ω)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- The natural map from a nonsingular point on a Weierstrass curve in affine coordinates to its
corresponding nonsingular projective point.  -/
WeierstrassCurve.Projective.Point.fromAffine : {R : Type r} →
  [inst : CommRing R] → {W' : WeierstrassCurve.Projective R} → [Nontrivial R] → W'.toAffine.Point → W'.Point
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- A Hamiltonian graph is a graph that contains a Hamiltonian cycle.

This is equivalent to there being an Hamiltonian cycle based at each vertex.
See `IsHamiltonian.exists_isHamiltonianCycle`.

By convention, the singleton graph is considered to be Hamiltonian and the empty graph is not.  -/
SimpleGraph.IsHamiltonian : {α : Type u_1} → [DecidableEq α] → [Fintype α] → SimpleGraph α → Prop
-- Std.Http.Protocol.H1
/-- Monotonic keep-alive update: once `keepAlive` is false it never flips back.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.updateKeepAlive : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool → Std.Http.Protocol.H1.Machine dir
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageMap.factor_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g)
  (m : CategoryTheory.Limits.ImageMap sq) {Z : C} (h : CategoryTheory.Limits.image g.hom ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f.hom)
      (CategoryTheory.CategoryStruct.comp m.map h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage g.hom) h)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_insertMany_list_le : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {l : List (α × β)}, (m.insertMany l).size ≤ m.size + l.length
-- Mathlib.Topology.Constructions.SumProd
Topology.IsClosedEmbedding.prodMap : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : X → Y} {g : Z → W},
  Topology.IsClosedEmbedding f → Topology.IsClosedEmbedding g → Topology.IsClosedEmbedding (Prod.map f g)
-- Mathlib.Order.CompleteLattice.Defs
/-- `(· \ a)` is left adjoint to `(· ⊔ a)`  -/
CompleteLinearOrder.sdiff_le_iff : ∀ {α : Type u_8} [self : CompleteLinearOrder α] (a b c : α), a \ b ≤ c ↔ a ≤ max b c
-- Mathlib.LinearAlgebra.Pi
LinearMap.ker_pi : ∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  {φ : ι → Type i} [inst_3 : (i : ι) → AddCommMonoid (φ i)] [inst_4 : (i : ι) → Module R (φ i)]
  (f : (i : ι) → M₂ →ₗ[R] φ i), (LinearMap.pi f).ker = ⨅ i, (f i).ker
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_lt_iff : ∀ {α : Type u_1} [inst : EDist α] {s : Set α} {d : ENNReal}, s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d
-- Mathlib.Data.Stream.Init
Stream'.take.eq_1 : ∀ {α : Type u} (x : Stream' α), Stream'.take 0 x = []
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.comap_isInducing_of_surjective : ∀ {R : Type u} (S : Type v) [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  Function.Surjective ⇑f → Topology.IsInducing (PrimeSpectrum.comap f)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.lift_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T}
  (s : (CategoryTheory.Functor.const J).obj X ⟶ D) (j : J),
  (CategoryTheory.Under.lift D s).obj j = CategoryTheory.Under.mk (s.app j)
-- Mathlib.Order.Category.BoolAlg
BoolAlg.instCategory : CategoryTheory.Category.{u, u + 1} BoolAlg
-- Mathlib.Data.Finset.Attach
Finset.attach_val : ∀ {α : Type u_1} (s : Finset α), s.attach.val = s.val.attach
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.powerlt_aleph0 : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c ^< Cardinal.aleph0 = c
-- Mathlib.RingTheory.Ideal.Prime
Ideal.one_notMem : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α) [hI : I.IsPrime], 1 ∉ I
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_add_right_eq_map : ∀ {m n : ℤ}, (m<...=m + n).toList = List.map (fun x => x + m + 1) (0...n).toList
-- Mathlib.Data.Num.Lemmas
PosNum.cast_to_int : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (n : PosNum), ↑↑n = ↑n
-- Lean.Parser.Basic
Lean.Parser.manyFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∈ Std.ExtDHashMap.Const.alter m k f ↔ (f (Std.ExtDHashMap.Const.get? m k)).isSome = true
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_alter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] (h : (↑m).WF) {k k' : α} {f : Option (β k) → Option (β k)}
  (hc : (m.alter k f).contains k' = true),
  (m.alter k f).get k' hc = if heq : (k == k') = true then cast ⋯ ((f (m.get? k)).get ⋯) else m.get k' ⋯
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.cons_support_tail : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, ¬p.Nil → u :: p.tail.support = p.support
-- Mathlib.Computability.Primrec.Basic
Primrec₂.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable β]
  [inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : β → γ → σ} {g : α → β} {h : α → γ},
  Primrec₂ f → Primrec g → Primrec h → Primrec fun a => f (g a) (h a)
-- Mathlib.Tactic.Widget.StringDiagram
/-- The list of nodes associated with a 2-morphism. The position is counted from the
specified natural numbers.  -/
Mathlib.Tactic.BicategoryLike.HorizontalComp.nodes : ℕ → ℕ → ℕ → Mathlib.Tactic.BicategoryLike.HorizontalComp → List Mathlib.Tactic.Widget.StringDiagram.Node
-- Lean.Elab.Term
/-- Marks an elaborator (tactic or command, currently) as supporting incremental elaboration.

For unmarked elaborators, the corresponding snapshot bundle field in the elaboration context is
unset so as to prevent accidental, incorrect reuse.
 -/
Lean.Elab.incrementalAttr : Lean.TagAttribute
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k : α} {h' : k ∈ t.insertMany l} (contains : k ∈ t), (t.insertMany l).get k h' = t.get k contains
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_eq_of_norm_add_lt_left : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℚ_[p]}, ‖z1 + z2‖ < ‖z1‖ → ‖z1‖ = ‖z2‖
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.generators.σ : ∀ {n : ℕ} (i : Fin (n + 1)), SimplexCategoryGenRel.generators (SimplexCategoryGenRel.σ i)
-- Init.Data.Slice.Array.Iterator
Array.instReprSubarray : {α : Type u} → [Repr α] → Repr (Subarray α)
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.radius_eq_ediam_iff : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α], G.radius = G.ediam ↔ ∃ e, ∀ (u : α), G.eccent u = e
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.equivOfEq_rfl : ∀ {F : Type u_4} [inst : Field F] {E : Type u_5} [inst_1 : Field E] [inst_2 : Algebra F E] (S : IntermediateField F E),
  IntermediateField.equivOfEq ⋯ = AlgEquiv.refl
-- Mathlib.NumberTheory.Niven
/-- `cos(q * π)` for `q : ℚ` is algebraic over `ℤ`, using the real `cos` function.  -/
Real.isAlgebraic_cos_rat_mul_pi : ∀ (q : ℚ), IsAlgebraic ℤ (Real.cos (↑q * Real.pi))
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Set.Finite.toFinset_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] [inst_1 : DecidableEq β] {s : Set α} {t : Set β} (hs : s.Finite)
  (ht : t.Finite) (hf : optParam (s +ᵥ t).Finite ⋯), hf.toFinset = hs.toFinset +ᵥ ht.toFinset
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.ofUpper_toUpper : ∀ {α : Type u_1} (a : α), Topology.WithUpper.ofUpper (Topology.WithUpper.toUpper a) = a
-- Mathlib.GroupTheory.Exponent
/-- If an element in a group has order two, then it is its own inverse.  -/
inv_eq_self_of_orderOf_eq_two : ∀ {G : Type u} [inst : Group G] {x : G}, orderOf x = 2 → x⁻¹ = x
-- Mathlib.Order.Interval.Set.SuccPred
Set.Icc_pred_right_eq_Ico_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {b : α},
  ¬IsMin b → ∀ (a : α), Set.Icc a (Order.pred b) = Set.Ico a b
-- Lean.Compiler.IR.CompilerM
Lean.IR.findDecl' : Lean.Name → Array Lean.IR.Decl → Lean.IR.CompilerM (Option Lean.IR.Decl)
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.moduleEndSelfOp_apply_apply : ∀ (R : Type u_1) {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s a : A),
  ((AlgEquiv.moduleEndSelfOp R) s) a = s * a
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.addRup : {β : Type u} → {α : Type v} → ℕ → β → Array ℕ → Std.Tactic.BVDecide.LRAT.Action β α