mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.isoOfHom.congr_simp : ∀ {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] (L : CategoryTheory.Functor C D)
  (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1) [inst_2 : L.IsLocalization W] {X Y : C} (f f_1 : X ⟶ Y)
  (e_f : f = f_1) (hf : W f),
  CategoryTheory.Localization.isoOfHom L W f hf = CategoryTheory.Localization.isoOfHom L W_1 f_1 ⋯
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.coe_finsupport : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M),
  ↑(ρ.finsupport x₀) = Function.support fun i => (ρ i) x₀
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.iterate_comp_eval : ∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R} (k : ℕ) (t : R),
  Polynomial.eval t (p.comp^[k] q) = (fun x => Polynomial.eval x p)^[k] (Polynomial.eval t q)
-- Aesop.RuleSet
Aesop.LocalRuleSet.toBaseRuleSet : Aesop.LocalRuleSet → Aesop.BaseRuleSet
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.isColimitCofanMapObjComp.eq_1 : ∀ {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) (q : J → K) (r : I → K) (hpqr : ∀ (i : I), q (p i) = r i) (k : K)
  (c : (j : J) → q j = k → X.CofanMapObjFun p j)
  (hc : (j : J) → (hj : q j = k) → CategoryTheory.Limits.IsColimit (c j hj))
  (c' : CategoryTheory.Limits.Cofan fun j => (c ↑j ⋯).pt) (hc' : CategoryTheory.Limits.IsColimit c'),
  X.isColimitCofanMapObjComp p q r hpqr k c hc c' hc' =
    CategoryTheory.Limits.Cofan.IsColimit.mk (X.cofanMapObjComp p q r hpqr k c c')
      (fun s =>
        CategoryTheory.Limits.Cofan.IsColimit.desc hc' fun x =>
          match x with
          | ⟨j, hj⟩ =>
            CategoryTheory.Limits.Cofan.IsColimit.desc (hc j hj) fun x =>
              match x with
              | ⟨i, hi⟩ => s.inj ⟨i, ⋯⟩)
      ⋯ ⋯
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.eraseList.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)) (hd : α) (tl : List α),
  Std.Internal.List.eraseList l (hd :: tl) = Std.Internal.List.eraseList (Std.Internal.List.eraseKey hd l) tl
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true ↔ t = ∅
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.gFunctor_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S T : CategoryTheory.ShortComplex C} (f : S ⟶ T),
  CategoryTheory.ShortComplex.gFunctor.map f = CategoryTheory.Arrow.homMk f.τ₂ f.τ₃ ⋯
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Closedness of `carrier`.  -/
SymbolicDynamics.FullShift.Subshift.isClosed : ∀ {A : Type u_1} [inst : TopologicalSpace A] {G : Type u_2} [inst_1 : AddMonoid G]
  (self : SymbolicDynamics.FullShift.Subshift A G), IsClosed self.carrier
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.then.eq_2 : ∀ (fs : Turing.ToPartrec.Code) (as : List ℕ) (k : Turing.ToPartrec.Cont),
  (Turing.ToPartrec.Cont.cons₁ fs as k).then = fun k' => Turing.ToPartrec.Cont.cons₁ fs as (k.then k')
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.apply_eq_iff_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N) {x y : M}, e x = e y ↔ x = y
-- Lean.Environment
/-- Constructs environment from `importModulesCore` results.

See also `importModules` for parameter documentation.
 -/
Lean.finalizeImport : Lean.ImportState →
  Array Lean.Import →
    Lean.Options →
      optParam UInt32 0 →
        Bool →
          Bool →
            (level : optParam Lean.OLeanLevel Lean.OLeanLevel.private) →
              optParam Bool (level != Lean.OLeanLevel.private) → optParam Bool false → IO Lean.Environment
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsFraisse.amalgamation : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K],
  FirstOrder.Language.Amalgamation K
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.pre.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasLimit F] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasLimit (E.comp F)],
  CategoryTheory.Limits.limit.pre F E =
    CategoryTheory.Limits.limit.lift (E.comp F)
      (CategoryTheory.Limits.Cone.whisker E (CategoryTheory.Limits.limit.cone F))
-- Init.Data.Slice.Basic
Std.Slice.mk.sizeOf_spec : ∀ {γ : Type u} [inst : SizeOf γ] (internalRepresentation : γ),
  sizeOf { internalRepresentation := internalRepresentation } = 1 + sizeOf internalRepresentation
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- If a function is differentiable around `x`, and has two derivatives at `x`, then the second
derivative is symmetric. Version over `ℝ`. See `second_derivative_symmetric_of_eventually` for a
version over `ℝ` or `ℂ`.  -/
second_derivative_symmetric_of_eventually_of_real : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {x : E} {f : E → F} {f' : E → E →L[ℝ] F} {f'' : E →L[ℝ] E →L[ℝ] F},
  (∀ᶠ (y : E) in nhds x, HasFDerivAt f (f' y) y) → HasFDerivAt f' f'' x → ∀ (v w : E), (f'' v) w = (f'' w) v
-- Batteries.Tactic.Init
/-- The `conv` mode tactic `equals e` claims that the currently focused subexpression is equal
to the term `e`, and proves this claim using the given tactic.
```
example (P : (Nat → Nat) → Prop) : P (fun n => n - n) := by
  conv in (_ - _) => equals 0 =>
    -- current goal: ⊢ n - n = 0
    apply Nat.sub_self
  -- current goal: P (fun n => 0)
```
 -/
Batteries.Tactic.Conv.equals : Lean.ParserDescr
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.card_nsmul_le : ∀ {G : Type u_1} [inst : AddGroup G] {K : ℝ} [inst_1 : DecidableEq G] {A : Finset G},
  IsApproximateAddSubgroup K ↑A → ∀ {n : ℕ}, ↑(n • A).card ≤ K ^ (n - 1) * ↑A.card
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.union_ae_eq_left_of_ae_eq_empty : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, t =ᵐ[μ] ∅ → s ∪ t =ᵐ[μ] s
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.seq.eq_def : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (w₁ : NumberField.InfinitePlace K) {B : ℕ}
  (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B)
  (x : ℕ),
  NumberField.Units.dirichletUnitTheorem.seq K w₁ hB x =
    match x with
    | 0 => ⟨1, ⋯⟩
    | n.succ => ⟨⋯.choose, ⋯⟩
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.mdifferentiableAt_section_of_subsingleton : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {s : (x : B) → E x} {x : B}
  [Subsingleton F], MDiffAt (T% s) x
-- Mathlib.Analysis.MeanInequalities
Real.geom_mean_eq_arith_mean_weighted_of_constant : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ) (x : ℝ),
  (∀ i ∈ s, 0 ≤ w i) →
    ∑ i ∈ s, w i = 1 → (∀ i ∈ s, 0 ≤ z i) → (∀ i ∈ s, w i ≠ 0 → z i = x) → ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorizationAt.mul : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A},
  g.IsWeierstrassFactorizationAt f h I →
    ∀ {g' : PowerSeries A} {f' : Polynomial A} {h' : PowerSeries A},
      g'.IsWeierstrassFactorizationAt f' h' I → (g * g').IsWeierstrassFactorizationAt (f * f') (h * h') I
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.small_Iio : ∀ (o : Ordinal.{u}), Small.{u, u + 1} ↑(Set.Iio o)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isEmbedding_coe : ∀ {α : Type u_1} [inst : TopologicalSpace α], Topology.IsEmbedding SetLike.coe
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.det_ne_zero : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [Nontrivial R]
  (g : GL n R), (↑g).det ≠ 0
-- Mathlib.NumberTheory.GaussSum
/-- For every finite field `F` of odd characteristic, we have `2^(#F/2) = χ₈ #F` in `F`.  -/
FiniteField.two_pow_card : ∀ {F : Type u_1} [inst : Fintype F] [inst_1 : Field F],
  ringChar F ≠ 2 → 2 ^ (Fintype.card F / 2) = ↑(ZMod.χ₈ ↑(Fintype.card F))
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Modification.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Lax.LaxTrans.Modification η θ},
  x = y ↔ x.app = y.app
-- Init.Data.Bool
Bool.eq_or_not_self : ∀ {a b : Bool}, b = (a || !b) ↔ a = true ∧ b = true
-- Init.Data.Array.Lemmas
Array.push_inj_left : ∀ {α : Type u_1} {a : α} {xs ys : Array α}, xs.push a = ys.push a ↔ xs = ys
-- Mathlib.Logic.Equiv.Fin.Basic
Int.divModEquiv_apply : ∀ (n : ℕ) [inst : NeZero n] (a : ℤ), (Int.divModEquiv n) a = (a / ↑n, Fin.ofNat n (a.natMod ↑n))
-- Mathlib.Order.Category.PartOrdEmb
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
PartOrdEmb.Hom.Simps.hom : (X Y : PartOrdEmb) → X.Hom Y → ↑X ↪o ↑Y
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.centralizer_univ : ∀ (M : Type u_1) [inst : AddMonoid M], AddSubmonoid.centralizer Set.univ = AddSubmonoid.center M
-- Batteries.Data.MLList.Basic
/-- Add one element to the end of a monadic lazy list.  -/
MLList.concat : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → α → MLList m α
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm of a difference is at most the max of each component. Restates the archimedean
property of the `p`-adic norm.  -/
padicNorm.sub : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ}, padicNorm p (q - r) ≤ max (padicNorm p q) (padicNorm p r)
-- Lean.Server.FileWorker.RequestHandling
_private.Lean.Server.FileWorker.RequestHandling.0.Lean.Server.FileWorker.handleFoldingRange.addRangeFromSyntax : Lean.FileMap → Lean.Lsp.FoldingRangeKind → Lean.Syntax → StateT (Array Lean.Lsp.FoldingRange) Lean.Server.RequestM Unit
-- Mathlib.Order.Heyting.Basic
compl_ne_self : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α} [Nontrivial α], aᶜ ≠ a
-- Mathlib.RepresentationTheory.Intertwining
/-- An intertwining map constructed form the linear map and the fact that it is intertwining.  -/
LinearMap.intertwiningMap_of_isIntertwiningMap : {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) →
                        (f : V →ₗ[A] W) → (∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)) → ρ.IntertwiningMap σ
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing : {α : Type u} → [self : NonUnitalNonAssocCommRing α] → NonUnitalNonAssocRing α
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.val : Lean.Expr → Lean.Meta.Match.Pattern
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.finite_iUnion_right_iff : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ι : Type u_3} {I : Set ι},
  I.Finite → ∀ {s : Set X} {t : ι → Set X}, Metric.AreSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Metric.AreSeparated s (t i)
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.mapₐ_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_5} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {B : Type u_6}
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (Aₚ : Type u_7) [inst_5 : CommSemiring Aₚ] [inst_6 : Algebra A Aₚ]
  [inst_7 : Algebra R Aₚ] [inst_8 : IsScalarTower R A Aₚ] (Bₚ : Type u_8) [inst_9 : CommSemiring Bₚ]
  [inst_10 : Algebra B Bₚ] [inst_11 : Algebra R Bₚ] [inst_12 : IsScalarTower R B Bₚ] (f : A →ₐ[R] B) (a : A)
  [inst_13 : IsLocalization.Away a Aₚ] [inst_14 : IsLocalization.Away (f a) Bₚ] (x : Aₚ),
  (IsLocalization.Away.mapₐ Aₚ Bₚ f a) x = (IsLocalization.Away.map Aₚ Bₚ f.toRingHom a) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₂ = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k (m₁.union m₂ ⋯ ⋯) = true}, (m₁.union m₂ ⋯ ⋯).getKey k h' = m₁.getKey k ⋯
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- If a free module has `Module.finrank` equal to `1`, then its special linear group is trivial.  -/
SpecialLinearGroup.subsingleton_of_finrank_eq_one : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] [Module.Free R V],
  Module.finrank R V = 1 → Subsingleton (SpecialLinearGroup R V)
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.isLink_iff_sym2_eq : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β},
  G.IsLink e x y → ∀ {x' y' : α}, G.IsLink e x' y' ↔ s(x, y) = s(x', y')
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_eq_sub : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoDiv hp a b = toIcoDiv hp 0 (b - a)
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticAt.aeval_mvPolynomial : ∀ {𝕜 : Type u_1} {E : Type u_2} {A : Type u_3} {B : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : CommSemiring A] {z : E}
  [inst_4 : NormedCommRing B] [inst_5 : NormedAlgebra 𝕜 B] [inst_6 : Algebra A B] {σ : Type u_5} {f : E → σ → B},
  (∀ (i : σ), AnalyticAt 𝕜 (fun x => f x i) z) →
    ∀ (p : MvPolynomial σ A), AnalyticAt 𝕜 (fun x => (MvPolynomial.aeval (f x)) p) z
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_sub' : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a b : ℚ},
  ↑a.den ≠ 0 →
    ↑b.den ≠ 0 →
      Lean.Grind.Field.NormNum.ofRat (a - b) = Lean.Grind.Field.NormNum.ofRat a - Lean.Grind.Field.NormNum.ofRat b
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.term.inj : ∀ {term : Lean.Term} {expr : Lean.Expr} {term_1 : Lean.Term} {expr_1 : Lean.Expr},
  Aesop.ElabRuleTerm.term term expr = Aesop.ElabRuleTerm.term term_1 expr_1 → term = term_1 ∧ expr = expr_1
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_pow : ∀ {m : Type u_2} {α : Type v} [inst : Semiring α] [inst_1 : StarRing α] [inst_2 : Fintype m] [inst_3 : DecidableEq m]
  (M : Matrix m m α) (k : ℕ), (M ^ k).conjTranspose = M.conjTranspose ^ k
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i),
  HomologicalComplex.homotopyCofiber.inlX φ i j hij = HomologicalComplex.homotopyCofiber.inlX φ i j hij
-- Init.Data.List.Lemmas
List.filter_eq_append_iff : ∀ {α : Type u_1} {l L₁ L₂ : List α} {p : α → Bool},
  List.filter p l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂
-- Lean.Environment
/-- Saved options. Empty for imported constants.  -/
_private.Lean.Environment.0.Lean.RealizationContext.opts : Lean.RealizationContext✝ → Lean.Options
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β},
  Std.DHashMap.Const.getD (m₁.diff m₂) k fallback = if k ∈ m₂ then fallback else Std.DHashMap.Const.getD m₁ k fallback
-- Init.Grind.Norm
Lean.Grind.forall_imp_eq_or : ∀ {α : Sort u_1} (p : α → Prop) (q : Prop), ((∀ (a : α), p a) → q) = ((∃ a, ¬p a) ∨ q)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mrefinePat#_» : Lean.ParserDescr
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extendedHom.congr_simp : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L], FractionalIdeal.extendedHom L B = FractionalIdeal.extendedHom L B
-- Lean.Parser.Extra
_private.Lean.Parser.Basic.0.Lean.Parser.addQuotDepth.parenthesizer : ℤ → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.IsCyclicallyReduced.singleton : ∀ {α : Type u} {x : α × Bool}, FreeGroup.IsCyclicallyReduced [x]
-- Batteries.Data.Nat.Bisect
Nat.le_add_one_of_avg_eq_left : ∀ {a b : ℕ}, a.avg b = a → b ≤ a + 1
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.composePath_mem_of_length_pos : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [W.IsStableUnderComposition] {X Y : C} {p : Quiver.Path X Y},
  W.paths p → 0 < p.length → W (CategoryTheory.composePath p)
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- The definition of a periodic orbit, in terms of `List.map`.  -/
Function.periodicOrbit_def : ∀ {α : Type u_1} (f : α → α) (x : α),
  Function.periodicOrbit f x = ↑(List.map (fun n => f^[n] x) (List.range (Function.minimalPeriod f x)))
-- Mathlib.RingTheory.Derivation.ToSquareZero
liftOfDerivationToSquareZero_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal B) [inst_5 : Algebra A B] [inst_6 : IsScalarTower R A B]
  (hI : I ^ 2 = ⊥) (f : Derivation R A ↥I) (x : A),
  (liftOfDerivationToSquareZero I hI f) x = ↑(f x) + (algebraMap A B) x
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.map_join : ∀ {α : Type u} {β : Type v} (f : α → β) (S : Stream'.WSeq (Stream'.WSeq α)),
  Stream'.WSeq.map f S.join = (Stream'.WSeq.map (Stream'.WSeq.map f) S).join
-- Mathlib.Data.Nat.Squarefree
Nat.squarefree_mul_iff : ∀ {m n : ℕ}, Squarefree (m * n) ↔ m.Coprime n ∧ Squarefree m ∧ Squarefree n
-- Std.Data.DHashMap.Internal.Defs
/-- This is the actual well-formedness predicate for hash maps. Users should never need to interact
with this and should use `WF` instead.  -/
Std.DHashMap.Internal.Raw.WFImp : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → Prop
-- Mathlib.CategoryTheory.Filtered.Basic
/-- The morphisms from `inf O H`.
 -/
CategoryTheory.IsCofiltered.infTo : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofiltered C] →
      (O : Finset C) →
        (H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))) →
          {X : C} → X ∈ O → (CategoryTheory.IsCofiltered.inf O H ⟶ X)
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atTop : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] [inst_3 : StandardBorelSpace Ω] (hm : m ≤ m0)
  [inst_4 : MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iCondIndep m hm s μ →
      ∀ {t : Set Ω},
        MeasurableSet t → ∀ᵐ (ω : Ω) ∂μ, μ[t.indicator fun ω => 1 | m] ω = 0 ∨ μ[t.indicator fun ω => 1 | m] ω = 1
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.IsSubterminal.isoDiag_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C} (hA : CategoryTheory.IsSubterminal A)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A], hA.isoDiag.inv = CategoryTheory.Limits.diag A
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.toSubgroup_inf : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {U V : OpenSubgroup G}, ↑(U ⊓ V) = ↑U ⊓ ↑V
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.of_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] (Z : C),
  CategoryTheory.InjectiveResolution.of Z =
    { cocomplex := CategoryTheory.InjectiveResolution.ofCocomplex Z, injective := ⋯, hasHomology := ⋯,
      ι :=
        ((CategoryTheory.InjectiveResolution.ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨CategoryTheory.Injective.ι Z, ⋯⟩,
      quasiIso := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.mk.congr_simp : ∀ {X : SSet} {n : ℕ} (x x_1 : X.obj (Opposite.op { len := n })) (e_x : x = x_1) (hx : x ∈ X.nonDegenerate n),
  SSet.N.mk x hx = SSet.N.mk x_1 ⋯
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.map_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g] (x : CategoryTheory.Subobject X),
  (CategoryTheory.Subobject.map (CategoryTheory.CategoryStruct.comp f g)).obj x =
    (CategoryTheory.Subobject.map g).obj ((CategoryTheory.Subobject.map f).obj x)
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instMin : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → Min (CategoryTheory.Precoverage C)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.sum_le_of_monotoneOn_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α} {m n : ℕ}
  {u : ℕ → α},
  MonotoneOn u (Set.Icc m n) →
    (∀ i ∈ Set.Icc m n, u i ∈ s) → ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
-- Mathlib.Order.SetDissipate
Set.dissipate_zero_nat : ∀ {β : Type u_2} (s : ℕ → Set β), Set.dissipate s 0 = s 0
-- Mathlib.Algebra.Order.Sub.Defs
AddLECancellable.lt_add_of_tsub_lt_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable b → a - b < c → a < b + c
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.pow_lt_iff_lt_log : ∀ {x y : ℝ} {n : ℕ}, 0 < x → 0 < y → (x ^ n < y ↔ ↑n * Real.log x < Real.log y)
-- Lean.Server.References
/-- Reads and parses the .ilean file at `path`.  -/
Lean.Server.Ilean.load : System.FilePath → IO Lean.Server.Ilean
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr : Type
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.codRestrict_apply_coe : ∀ {M : Type u_1} {N : Type u_2} {σ : Type u_4} [inst : Add M] [inst_1 : Add N] [inst_2 : SetLike σ N]
  [inst_3 : AddMemClass σ N] (f : M →ₙ+ N) (S : σ) (h : ∀ (x : M), f x ∈ S) (n : M), ↑((f.codRestrict S h) n) = f n