mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Util.AtLocation
Mathlib.Tactic.instReprBehaviorIfUnchanged.repr : Mathlib.Tactic.BehaviorIfUnchanged → ℕ → Std.Format
-- Lean.Parser.Do
Lean.Parser.Term.doHave.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
TensorAlgebra.toExterior_ι : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (m : M),
  TensorAlgebra.toExterior ((TensorAlgebra.ι R) m) = (ExteriorAlgebra.ι R) m
-- Std.Time.Date.Unit.Week
/-- Convert `Week.Offset` into `Minute.Offset`.
 -/
Std.Time.Week.Offset.toMinutes : Std.Time.Week.Offset → Std.Time.Minute.Offset
-- Lean.Parser.Command
Lean.Parser.Command.partial : Lean.Parser.Parser
-- Mathlib.Data.FP.Basic
FP.emax : [C : FP.FloatCfg] → ℕ
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_asymm : ∀ {x y : ZFSet.{u_1}}, x ∈ y → y ∉ x
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.toSearcher_eq : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice},
  String.Slice.Pattern.ToForwardSearcher.toSearcher p s =
    String.Slice.Pattern.ToForwardSearcher.toSearcher (fun x => decide (p x)) s
-- Mathlib.LinearAlgebra.Matrix.Unique
Matrix.uniqueRingEquiv_apply : ∀ {m : Type u_1} {A : Type u_3} [inst : Unique m] [inst_1 : NonUnitalNonAssocSemiring A] (M : Matrix m m A),
  Matrix.uniqueRingEquiv M = M default default
-- Init.Data.Nat.Lemmas
Nat.max_add_left_self : ∀ {a b : ℕ}, max a (b + a) = b + a
-- Mathlib.GroupTheory.GroupAction.FixedPoints
AddAction.mem_fixedBy_zsmul : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g : G} {a : α},
  a ∈ AddAction.fixedBy α g → ∀ (j : ℤ), a ∈ AddAction.fixedBy α (j • g)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.foldl_eq_foldl_toList : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α_1 → α → α_1} {init : α_1} {t : RBTree.RBNode.Stream α},
  RBTree.RBNode.Stream.foldl f init t = List.foldl f init t.toList
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.pderiv_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ}, (MvPowerSeries.pderiv R i) 1 = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_dblZ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).dblZ (⇑f ∘ P) = f (W'.dblZ P)
-- Mathlib.RingTheory.Localization.BaseChange
/-- The forward direction of `isLocalizedModule_iff_isBaseChange`. It is also used to prove the
other direction.  -/
IsLocalizedModule.isBaseChange : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A] {M : Type u_3} [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  {M' : Type u_4} [inst_6 : AddCommMonoid M'] [inst_7 : Module R M'] [inst_8 : Module A M']
  [inst_9 : IsScalarTower R A M'] (f : M →ₗ[R] M') [IsLocalizedModule S f], IsBaseChange A f
-- Lean.Environment
/-- Resulting "async branch" environment which should be used to add the desired declaration in a new
task and then call `AddConstAsyncResult.commit*` to commit results back to the main environment.
`commitCheckEnv` completes the addition; if it is not called and the `AddConstAsyncResult` object
is dropped, `sorry`ed default values will be reported instead and the kernel environment will be
left unchanged.
 -/
Lean.Environment.AddConstAsyncResult.asyncEnv : Lean.Environment.AddConstAsyncResult → Lean.Environment
-- Mathlib.Analysis.Normed.Group.Basic
nndist_eq_nnnorm_div : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (a b : E), nndist a b = ‖a / b‖₊
-- Mathlib.Algebra.Lie.Killing
/-- Given a Killing Lie algebra `L`, if `L'` is isomorphic to `L`, then `L'` is Killing too.  -/
LieAlgebra.isKilling_of_equiv : ∀ {R : Type u_1} {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L' : Type u_4}
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] [LieAlgebra.IsKilling R L] (e : L ≃ₗ⁅R⁆ L'),
  LieAlgebra.IsKilling R L'
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instZero : {M : Type u_1} → [Zero M] → [inst : Monoid M] → Zero (Associates M)
-- Mathlib.Algebra.GroupWithZero.Action.Center
Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe : ∀ (G₀ : Type u_1) [inst : GroupWithZero G₀] (u : (↥(Submonoid.center G₀))ˣ),
  ↑↑((Subgroup.centerUnitsEquivUnitsCenter G₀).symm u) = ↑↑u
-- Mathlib.Probability.Independence.Basic
/-- A family of functions defined on the same space `Ω` and taking values in possibly different
spaces, each with a measurable space structure, is independent if the family of measurable space
structures they generate on `Ω` is independent. For a function `g` with codomain having measurable
space structure `m`, the generated measurable space structure is `MeasurableSpace.comap g m`.  -/
ProbabilityTheory.iIndepFun : {Ω : Type u_1} →
  {ι : Type u_2} →
    {_mΩ : MeasurableSpace Ω} →
      {β : ι → Type u_6} →
        [m : (x : ι) → MeasurableSpace (β x)] →
          ((x : ι) → Ω → β x) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.iIndepFun._auto_1 → Prop
-- Init.Data.Array.Lemmas
Array.filter_map : ∀ {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {xs : Array β},
  Array.filter p (Array.map f xs) = Array.map f (Array.filter (p ∘ f) xs)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.IsInitial.ord_card : ∀ {o : Ordinal.{u_1}}, o.IsInitial → o.card.ord = o
-- Mathlib.RingTheory.Ideal.Defs
/-- The subgroup of elements `g` of `G` such that `∀ x, g • x - x ∈ I`.  -/
Ideal.inertia : {α : Type u} → [inst : Ring α] → (G : Type u_1) → [inst_1 : Group G] → [MulAction G α] → Ideal α → Subgroup G
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- An iterated form of the Kruskal-Katona theorem. In particular, the minimum possible iterated
shadow size is attained by initial segments.  -/
Finset.iterated_kk : ∀ {n r k : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))},
  Set.Sized r ↑𝒜 →
    𝒞.card ≤ 𝒜.card → Finset.Colex.IsInitSeg 𝒞 r → (Finset.shadow^[k] 𝒞).card ≤ (Finset.shadow^[k] 𝒜).card
-- Init.Data.Array.Range
Array.find?_range_eq_none : ∀ {n : ℕ} {p : ℕ → Bool}, Array.find? p (Array.range n) = none ↔ ∀ i < n, (!p i) = true
-- Init.Data.SInt.Bitwise
instIdempotentOpInt32HAnd : Std.IdempotentOp fun x1 x2 => x1 &&& x2
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
/-- Let `f : E → F` be a function differentiable on a set `s` and continuous on its closure.
Let `a`, `b` be two points such that the open segment connecting `a` to `b` is a subset of `s`.

If `‖Df‖ ≤ C` everywhere on `s` then `‖f b - f a‖ ≤ C * volume u`,
where `u` is the set of points `t ∈ Ioo 0 1`
such that `f` has nonzero derivative at `lineMap a b t`.  -/
norm_sub_le_mul_volume_of_norm_fderiv_le : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {a b : E} {C : ℝ} {s : Set E},
  IsOpen s →
    DiffContOnCl ℝ f s →
      openSegment ℝ a b ⊆ s →
        (∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C) →
          ‖f b - f a‖ ≤
            C * ‖b - a‖ * MeasureTheory.volume.real {t | t ∈ Set.Ioo 0 1 ∧ fderiv ℝ f ((AffineMap.lineMap a b) t) ≠ 0}
-- Mathlib.Algebra.Order.Monoid.NatCast
ZeroLEOneClass.neZero.two : ∀ (α : Type u_1) [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftMono α],
  NeZero 2
-- Mathlib.LinearAlgebra.Complex.Module
ComplexStarModule.ext : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {x y : A}, realPart x = realPart y → imaginaryPart x = imaginaryPart y → x = y
-- Mathlib.LinearAlgebra.Finsupp.Pi
FunOnFinite.linearMap_id : ∀ (R : Type u_5) (M : Type u_6) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (X : Type u_7)
  [inst_3 : Finite X], FunOnFinite.linearMap R M id = LinearMap.id
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α}
  {h : k ∈ Std.ExtDHashMap.filterMap f m},
  Std.ExtDHashMap.Const.get (Std.ExtDHashMap.filterMap f m) k h =
    (f (m.getKey k ⋯) (Std.ExtDHashMap.Const.get m k ⋯)).get ⋯
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isInitial_iff_isEmpty : ∀ {X : AlgebraicGeometry.Scheme}, Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty ↥X
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.degBound_succ : ∀ (k : ℕ) (D : ℕ → ℕ) (n : ℕ),
  ChevalleyThm.MvPolynomialC.degBound k D (n + 1) =
    ChevalleyThm.MvPolynomialC.numBound k D (n + 1) ^ ChevalleyThm.MvPolynomialC.numBound k D (n + 1) *
      ChevalleyThm.MvPolynomialC.degBound k D n
-- Mathlib.Tactic.NormNum.IsCoprime
Mathlib.Meta.NormNum.isInt_not_isCoprime : ∀ {x y nx ny : ℤ}, Mathlib.Meta.NormNum.IsInt x nx → Mathlib.Meta.NormNum.IsInt y ny → ¬IsCoprime nx ny → ¬IsCoprime x y
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.root_mem_submodule_iff_of_add_mem_invtSubmodule : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {i j : ι}
  {K : Type u_5} [inst_2 : Field K] [NeZero 2] [inst_4 : Module K M] [inst_5 : Module K N] {P : RootPairing ι K M N}
  (q : ↥P.invtRootSubmodule), P.root i + P.root j ∈ Set.range ⇑P.root → (P.root i ∈ ↑q ↔ P.root j ∈ ↑q)
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.comp_app : ∀ {X Y Z : SSet} (f : X ⟶ Y) (g : Y ⟶ Z) (n : SimplexCategoryᵒᵖ),
  (CategoryTheory.CategoryStruct.comp f g).app n = CategoryTheory.CategoryStruct.comp (f.app n) (g.app n)
-- Mathlib.Data.EReal.Operations
EReal.top_mul_coe_of_pos : ∀ {x : ℝ}, 0 < x → ⊤ * ↑x = ⊤
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiff.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₂},
  ContMDiff I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n f →
    ContMDiff I (modelWithCornersSelf 𝕜 ((F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃)) n fun y =>
      ContinuousLinearMap.precomp F₃ (f y)
-- Mathlib.Algebra.QuadraticDiscriminant
discrim_eq_zero_iff : ∀ {K : Type u_1} [inst : Field K] [NeZero 2] {a b c : K},
  a ≠ 0 → (discrim a b c = 0 ↔ ∃! x, a * (x * x) + b * x + c = 0)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.range_awayMapAux_subset : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {e : ι} {f g : A},
  g ∈ 𝒜 e →
    ∀ {x : A} (hx : x = f * g),
      Set.range ⇑(HomogeneousLocalization.awayMapAux✝ 𝒜 ⋯) ⊆ Set.range HomogeneousLocalization.val
-- Batteries.Util.Cache
Batteries.Tactic.DeclCache.mk' : {α : Type} →
  Batteries.Tactic.Cache α →
    (Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α) →
      (Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α) → Batteries.Tactic.DeclCache α
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_comp_addMonoidHom : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (g f : CentroidHom α), ↑(g.comp f) = (↑g).comp ↑f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.cons_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v w v' w' : V} (h : G.Adj u v) (p : G.Walk v' w') (hv : v' = v) (hw : w' = w),
  SimpleGraph.Walk.cons h (p.copy hv hw) = (SimpleGraph.Walk.cons ⋯ p).copy ⋯ hw
-- Mathlib.Logic.Equiv.Set
/-- If `s` is a set with decidable membership, then the sum of `s ∪ t` and `s ∩ t` is equivalent
to `s ⊕ t`.  -/
Equiv.Set.unionSumInter : {α : Type u} → (s t : Set α) → [DecidablePred fun x => x ∈ s] → ↑(s ∪ t) ⊕ ↑(s ∩ t) ≃ ↑s ⊕ ↑t
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.addRightMono : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddMonoid N] [inst_2 : LinearOrder N]
  [AddRightStrictMono N], AddRightMono (Colex (α →₀ N))
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.cancelAux.match_3.splitter : (motive : ℕ → Sort u_1) → (fuel : ℕ) → (Unit → motive 0) → ((fuel : ℕ) → motive fuel.succ) → motive fuel
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
/-- Given an element `f` of a skew monoid algebra, `erase a f` is an element with the same coefficients
as `f` except at `a` where the coefficient is `0`.
If `a` is not in the support of `f` then `erase a f = f`.  -/
SkewMonoidAlgebra.erase : {M : Type u_4} → {α : Type u_5} → [inst : AddCommMonoid M] → α → SkewMonoidAlgebra M α →+ SkewMonoidAlgebra M α
-- Mathlib.LinearAlgebra.CrossProduct
/-- **Alias** of `cross_anticomm`. -/
neg_cross : ∀ {R : Type u_1} [inst : CommRing R] (v w : Fin 3 → R), -(crossProduct v) w = (crossProduct w) v
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_comm : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) (x : TensorProduct R N M),
  (TensorProduct.map f g) ((TensorProduct.comm R N M) x) = (TensorProduct.comm R₂ N₂ M₂) ((TensorProduct.map g f) x)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- `C^{n + 1}` is equivalent to `C^n` and the `n`-th derivative being `C^1`.  -/
contDiffOn_nat_succ_iff_contDiffOn_one_iteratedDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : ℕ},
  UniqueDiffOn 𝕜 s →
    (ContDiffOn 𝕜 (↑(n + 1)) f s ↔ ContDiffOn 𝕜 (↑n) f s ∧ ContDiffOn 𝕜 1 (iteratedDerivWithin n f s) s)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.finite_quotient_span_sub_one' : ∀ {p : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p),
  Finite (NumberField.RingOfIntegers K ⧸ Ideal.span {hζ.toInteger - 1})
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearEquiv.congrQuadraticMap_refl : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N],
  (LinearEquiv.refl R N).congrQuadraticMap = LinearEquiv.refl R (QuadraticMap R M N)
-- Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
/-- If `x` is close to `y` and `y` is close to `z`, then `x` and `z` are at least as close.  -/
Polynomial.cardPowDegree_anti_archimedean : ∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Field Fq] {x y z : Polynomial Fq} {a : ℤ},
  Polynomial.cardPowDegree (x - y) < a → Polynomial.cardPowDegree (y - z) < a → Polynomial.cardPowDegree (x - z) < a
-- Lean.Elab.Tactic.Induction
/-- The subgoal metavariable for the alternative.  -/
Lean.Elab.Tactic.ElimApp.Alt.mvarId : Lean.Elab.Tactic.ElimApp.Alt → Lean.MVarId
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.eq_1 : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig)
  (var : Std.Tactic.BVDecide.BVPred),
  Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig (Std.Tactic.BVDecide.BoolExpr.literal var) cache =
    Std.Tactic.BVDecide.BVPred.bitblast aig { val := var, cache := cache }
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.isEquivalent_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x →
    Topology.IsInducing ⇑f' → Asymptotics.IsEquivalent (nhdsWithin x s) (fun x_1 => f x_1 - f x) fun x_1 => f' (x_1 - x)
-- Mathlib.Data.Set.Lattice
Set.inter_iInter : ∀ {β : Type u_2} {ι : Sort u_5} [Nonempty ι] (s : Set β) (t : ι → Set β), s ∩ ⋂ i, t i = ⋂ i, s ∩ t i
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.combo.inj : ∀ {s t : Lean.Omega.Constraint} {x y : Lean.Omega.Coeffs} {a : ℤ} {j : Lean.Elab.Tactic.Omega.Justification s x} {b : ℤ}
  {k : Lean.Elab.Tactic.Omega.Justification t y} {j_1 : Lean.Elab.Tactic.Omega.Justification s x}
  {k_1 : Lean.Elab.Tactic.Omega.Justification t y},
  Lean.Elab.Tactic.Omega.Justification.combo a j b k = Lean.Elab.Tactic.Omega.Justification.combo a j_1 b k_1 →
    j = j_1 ∧ k = k_1
-- Mathlib.Data.Nat.Factorization.Basic
/-- Exactly `n / p` naturals in `[1, n]` are multiples of `p`.
See `Nat.card_multiples'` for an alternative spelling of the statement.  -/
Nat.card_multiples : ∀ (n p : ℕ), {e ∈ Finset.range n | p ∣ e + 1}.card = n / p
-- Aesop.RuleSet
Aesop.LocalRuleSet.applicableForwardRules : Aesop.LocalRuleSet → Lean.Expr → Lean.MetaM (Array (Aesop.ForwardRule × Aesop.PremiseIndex))
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.iUnion_finset_rightRel_eq_univ_of_rightRel : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} {t : Finset (DoubleCoset.Quotient ↑H ↑K)},
  Set.univ ⊆ ⋃ i ∈ t, Quot.mk ⇑(QuotientGroup.rightRel H) '' DoubleCoset.doubleCoset (Quotient.out i) ↑H ↑K →
    ⋃ q ∈ t, DoubleCoset.doubleCoset (Quotient.out q) ↑H ↑K = Set.univ
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsCoseparator.def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : C},
  CategoryTheory.IsCoseparator G →
    ∀ ⦃X Y : C⦄ (f g : X ⟶ Y),
      (∀ (h : Y ⟶ G), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) → f = g
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
MeasureTheory.lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero : ∀ {α : Type u_1} {E' : Type u_2} {𝕜 : Type u_4} {p : ENNReal} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E'] [inst_2 : InnerProductSpace 𝕜 E'] [CompleteSpace E']
  [inst_4 : NormedSpace ℝ E'],
  m ≤ m0 →
    ∀ (f : ↥(MeasureTheory.lpMeas E' 𝕜 m p μ)),
      p ≠ 0 →
        p ≠ ⊤ →
          (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑↑f) s μ) →
            (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0) → ↑↑↑f =ᵐ[μ] 0
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.rank_top' : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  Module.rank F ↥⊤ = Module.rank F E
-- Init.Data.Array.Lemmas
Array.size_replace : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {xs : Array α}, (xs.replace a b).size = xs.size
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.fromCols_one_isTotallyUnimodular_iff : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] [inst_1 : DecidableEq m] (A : Matrix m n R),
  (A.fromCols 1).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
-- Mathlib.Data.List.MinMax
List.not_maximum_lt_of_mem' : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] {l : List α} {a : α}, a ∈ l → ¬l.maximum < ↑a
-- Mathlib.Combinatorics.Quiver.Path
/-- Turn a path into a list. The list contains `a` at its head, but not `b` a priori.  -/
Quiver.Path.toList : {V : Type u} → [inst : Quiver V] → {a b : V} → Quiver.Path a b → List V
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.assignmentsInvariant_insertRatUnits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ratUnits = #[] ∧ f.AssignmentsInvariant →
    ∀ (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
      (f.insertRatUnits units).1.AssignmentsInvariant
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.mem_notConvergentSeq_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : PseudoEMetricSpace β] {n : ℕ} {j : ι} {f : ι → α → β} {g : α → β}
  [inst_1 : Preorder ι] {x : α},
  x ∈ MeasureTheory.Egorov.notConvergentSeq f g n j ↔ ∃ k ≥ j, (↑n)⁻¹ < edist (f k x) (g x)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgHom.mem_range_self : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (φ : F) (x : A),
  φ x ∈ NonUnitalStarAlgHom.range φ
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s₁ == s₂`  -/
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.StartsWithResult.exact : Lean.Grind.AC.StartsWithResult✝
-- Lean.Meta.LazyDiscrTree
/-- Create a key path from an expression we are matching against.

This should have mvars instantiated where feasible.
 -/
Lean.Meta.LazyDiscrTree.targetPath : Lean.Expr → Lean.MetaM (Array Lean.Meta.LazyDiscrTree.Key)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mkPrecomp_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {Y Y' : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) (g : Y' ⟶ Y),
  (CategoryTheory.CostructuredArrow.mkPrecomp f g).left = g
-- Mathlib.AlgebraicGeometry.Restrict
/-- The restriction of an isomorphism onto an open set.  -/
AlgebraicGeometry.Scheme.Hom.preimageIso : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → [CategoryTheory.IsIso f] → (U : Y.Opens) → ↑((TopologicalSpace.Opens.map f.base).obj U) ≅ ↑U
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k : α} [inst_3 : Inhabited (β k)],
  (List.map Sigma.fst l).contains k = false → (Std.DHashMap.Raw.ofList l).get! k = default
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instIsTorsionFree : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {S : Type u_10} [inst_5 : Semiring S]
  [inst_6 : Module S N] [inst_7 : SMulCommClass R S N] [Module.IsTorsionFree S N],
  Module.IsTorsionFree S (M [⋀^ι]→ₗ[R] N)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.le_strictLimitsClosureStep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)], P ≤ P.strictLimitsClosureStep J
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.lhomWithConstants.eq_1 : ∀ (L : FirstOrder.Language) (α : Type w'), L.lhomWithConstants α = FirstOrder.Language.LHom.sumInl
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- Natural isomorphisms between functors lift to commutative group objects.  -/
CategoryTheory.Functor.mapCommGrpNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.CartesianMonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F F' : CategoryTheory.Functor C D} →
                  [inst_6 : F.Braided] → [inst_7 : F'.Braided] → (F ≅ F') → (F.mapCommGrp ≅ F'.mapCommGrp)
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
NNReal.ball_zero_eq_Ico : ∀ (c : ℝ), Metric.ball 0 c = Set.Ico 0 c.toNNReal