mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- Any family is compressed along two identical elements.  -/
UV.isCompressed_self : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  [inst_3 : DecidableEq α] (u : α) (s : Finset α), UV.IsCompressed u u s
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.withInductiveLocalDecls.loop.eq_def : ∀ {α : Type} (rs : Array Lean.Elab.Command.PreElabHeaderResult)
  (x : Array Lean.Expr → Array Lean.Expr → Lean.Elab.TermElabM α) (params : Array Lean.Expr) (i : ℕ)
  (indFVars : Array Lean.Expr),
  Lean.Elab.Command.withInductiveLocalDecls.loop✝ rs x params i indFVars =
    if h : i < rs.size then
      have r := rs[i];
      have __s := Std.toStream r.origParams;
      do
      let _ ←
        forIn params __s fun param __s =>
            have __s := __s;
            match Std.Stream.next? __s with
            | none => pure (ForInStep.done __s)
            | some (origParam, s') =>
              have __s := s';
              match origParam with
              | Lean.Expr.fvar origFVar => do
                let __do_lift ← liftM param.fvarId!.getUserName
                Lean.Elab.pushInfoLeaf
                    (Lean.Elab.Info.ofFVarAliasInfo { userName := __do_lift, id := param.fvarId!, baseId := origFVar })
                pure (ForInStep.yield __s)
              | x => pure (ForInStep.yield __s)
      Lean.Meta.withAuxDecl r.view.shortDeclName r.type r.view.declName fun indFVar =>
          Lean.Elab.Command.withInductiveLocalDecls.loop✝ rs x params (i + 1) (indFVars.push indFVar)
    else x params indFVars
-- Mathlib.Tactic.FunProp.FunctionData
/-- Not a morphism application.  -/
Mathlib.Meta.FunProp.MorApplication.none : Mathlib.Meta.FunProp.MorApplication
-- Mathlib.SetTheory.Lists
Lists'.atom.injEq : ∀ {α : Type u} (a a_1 : α), (Lists'.atom a = Lists'.atom a_1) = (a = a_1)
-- Mathlib.Data.ZMod.Basic
/-- We have that `ringChar (ZMod n) = n`.  -/
ZMod.ringChar_zmod_n : ∀ (n : ℕ), ringChar (ZMod n) = n
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.mk.sizeOf_spec : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} [inst_4 : SizeOf A] [inst_5 : SizeOf G] [inst_6 : SizeOf W]
  (toSubmodule : Submodule A W) (apply_mem_toSubmodule : ∀ (g : G) ⦃v : W⦄, v ∈ toSubmodule → (ρ g) v ∈ toSubmodule),
  sizeOf { toSubmodule := toSubmodule, apply_mem_toSubmodule := apply_mem_toSubmodule } = 1 + sizeOf toSubmodule
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_biUnion_closure_eq_closure_biUnion : ∀ {ι : Type u_1} {α : Type u_2} (M : Matroid α) (Xs : ι → Set α) (A : Set ι),
  M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.IsBridge.anti : ∀ {V : Type u} {G G' : SimpleGraph V} {e : Sym2 V}, G ≤ G' → G'.IsBridge e → G.IsBridge e
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Any.eq_def : ∀ {α : Type u_1} (P : α → Prop) (x : Ordnode α),
  Ordnode.Any P x =
    match x with
    | Ordnode.nil => False
    | Ordnode.node size l x r => Ordnode.Any P l ∨ P x ∨ Ordnode.Any P r
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.hasIdealSupport_iff : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R},
  P.HasIdealSupport ↔ ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
IsBoundedBilinearMap.deriv.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f f_1 : E × F → G} (e_f : f = f_1)
  (h : IsBoundedBilinearMap 𝕜 f) (p p_1 : E × F), p = p_1 → h.deriv p = ⋯.deriv p_1
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.coeff_truncTotal_mul_truncTotal_eq_coeff_mul : ∀ {σ : Type u_1} {R : Type u_2} {n : ℕ} [inst : Finite σ] [inst_1 : CommSemiring R] (p q : MvPowerSeries σ R)
  {x : σ →₀ ℕ},
  Finsupp.degree x < n →
    MvPolynomial.coeff x ((MvPowerSeries.truncTotal n) p * (MvPowerSeries.truncTotal n) q) =
      (MvPowerSeries.coeff x) (p * q)
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Prequotient.one : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] → {F : CategoryTheory.Functor J MonCat} → MonCat.Colimits.Prequotient F
-- Mathlib.Order.Nucleus
Nucleus.mk.injEq : ∀ {X : Type u_2} [inst : SemilatticeInf X] (toInfHom : InfHom X X)
  (idempotent' : ∀ (x : X), toInfHom.toFun (toInfHom.toFun x) ≤ toInfHom.toFun x)
  (le_apply' : ∀ (x : X), x ≤ toInfHom.toFun x) (toInfHom_1 : InfHom X X)
  (idempotent'_1 : ∀ (x : X), toInfHom_1.toFun (toInfHom_1.toFun x) ≤ toInfHom_1.toFun x)
  (le_apply'_1 : ∀ (x : X), x ≤ toInfHom_1.toFun x),
  ({ toInfHom := toInfHom, idempotent' := idempotent', le_apply' := le_apply' } =
      { toInfHom := toInfHom_1, idempotent' := idempotent'_1, le_apply' := le_apply'_1 }) =
    (toInfHom = toInfHom_1)
-- Mathlib.CategoryTheory.Localization.Linear
CategoryTheory.Localization.functor_linear_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {E : Type u_1}
  [inst_4 : CategoryTheory.Category.{v_1, u_1} E] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [inst_6 : CategoryTheory.Preadditive E] (R : Type u_2)
  [inst_7 : Ring R] [inst_8 : CategoryTheory.Linear R C] [inst_9 : CategoryTheory.Linear R D]
  [inst_10 : CategoryTheory.Linear R E] [CategoryTheory.Functor.Linear R L] (F : CategoryTheory.Functor C E)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Localization.Lifting L W F G],
  CategoryTheory.Functor.Linear R F ↔ CategoryTheory.Functor.Linear R G
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- `SMulCommClass R' R'₂ M` implies `SMulCommClass R' R'₂ (M ⊗[R] N)`  -/
TensorProduct.smulCommClass_left : ∀ {R : Type u_1} {R' : Type u_4} [inst : CommSemiring R] [inst_1 : Monoid R'] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : DistribMulAction R' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMulCommClass R R' M] {R'₂ : Type u_22} [inst_8 : Monoid R'₂]
  [inst_9 : DistribMulAction R'₂ M] [inst_10 : SMulCommClass R R'₂ M] [SMulCommClass R' R'₂ M],
  SMulCommClass R' R'₂ (TensorProduct R M N)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.mem_sphere : ∀ {P : Type u_2} [inst : MetricSpace P] {p : P} {s : EuclideanGeometry.Sphere P}, p ∈ s ↔ dist p s.center = s.radius
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_nnnorm_eq_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (f : WithLp ⊤ (α × β)), ‖f‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_false : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {u : β → α},
  (Filter.bliminf u f fun x => False) = ⊤
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
/-- For all sets `s` in `(μ.sigmaFiniteSetWRT ν)ᶜ`, if `ν s ≠ 0` then `μ s = ∞`.  -/
MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α}
  [inst : MeasureTheory.IsFiniteMeasure ν], s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ → ν s ≠ 0 → μ s = ⊤
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Rel.in₁₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
  (a, b, c) ∈ t → SimpleGraph.TripartiteFromTriangles.Rel t (Sum3.in₁ b) (Sum3.in₂ c)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoElabM : Type → Type
-- Init.Data.Option.Attach
Option.isSome_unattach : ∀ {α : Type u_1} {p : α → Prop} {o : Option { x // p x }}, o.unattach.isSome = o.isSome
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The functor `X.HomotopyCategory ⥤ Y.HomotopyCategory ⥤ (X ⊗ Y).HomotopyCategory`
when `X` and `Y` are `2`-truncated simplicial sets.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.curriedInverse : (X Y : SSet.Truncated 2) →
  CategoryTheory.Functor X.HomotopyCategory
    (CategoryTheory.Functor Y.HomotopyCategory (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.toNonUnitalSubalgebra_subtype : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A),
  NonUnitalSubalgebraClass.subtype S = NonUnitalAlgHomClass.toNonUnitalAlgHom (NonUnitalStarSubalgebraClass.subtype S)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isLeftKanExtension_iff_postcomp₁ : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') [G.IsEquivalence] (e : L.comp G ≅ L') {F : CategoryTheory.Functor C H}
  {F' : CategoryTheory.Functor D' H} (α : F ⟶ L'.comp F'),
  F'.IsLeftKanExtension α ↔
    (G.comp F').IsLeftKanExtension
      (CategoryTheory.CategoryStruct.comp α
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e.inv F') (L.associator G F').hom))
-- Mathlib.GroupTheory.OrderOfElement
nsmul_ne_zero_of_lt_addOrderOf : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ}, n ≠ 0 → n < addOrderOf x → n • x ≠ 0
-- Mathlib.Order.Ideal
Order.Ideal.eq_sup_of_le_sup : ∀ {P : Type u_1} [inst : DistribLattice P] {I J : Order.Ideal P} {x i j : P},
  i ∈ I → j ∈ J → x ≤ i ⊔ j → ∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app : ∀ {X Y : AlgebraicGeometry.Scheme} {M : X.Modules} {f g : X ⟶ Y} (hf : f = g) (U : Y.Opens),
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.pushforwardCongr hf).hom.app M) U =
    M.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.le_basicOpen_pow : ∀ {R : Type u} [inst : CommSemiring R] (r : R) (n : ℕ), PrimeSpectrum.basicOpen r ≤ PrimeSpectrum.basicOpen (r ^ n)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.spanOp_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  (X_1 : CategoryTheory.Limits.WalkingSpan),
  (CategoryTheory.Limits.spanOp f g).hom.app X_1 =
    (match X_1 with
      | none => CategoryTheory.Iso.refl (Opposite.op Z)
      | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.op X)
      | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.op Y)).hom
-- Init.Data.String.Basic
String.toList_push : ∀ {s : String} (c : Char), (s.push c).toList = s.toList ++ [c]
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mapAlgHom.eq_1 : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] [inst_3 : Algebra R S₁] [inst_4 : Algebra R S₂] (f : S₁ →ₐ[R] S₂),
  MvPolynomial.mapAlgHom f = AddMonoidAlgebra.mapAlgHom (σ →₀ ℕ) f
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp_fix : ∀ (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp f.fix k =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal f.fix k) ∪
      Turing.PartrecToTM2.codeSupp f (Turing.PartrecToTM2.Cont'.fix f k)
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.hom_ext : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommRing k] [inst_1 : Monoid G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  {ρ : Representation k G V} {f g : ρ.Coinvariants →ₗ[k] W},
  f ∘ₗ Representation.Coinvariants.mk ρ = g ∘ₗ Representation.Coinvariants.mk ρ → f = g
-- Init.Data.Vector.Extract
Vector.getElem?_extract_of_lt : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j k : ℕ} (h : k < min j n - i), (xs.extract i j)[k]? = some xs[i + k]
-- Mathlib.Order.Concept
/-- Define a concept from an extent, by setting the intent to its upper polar.  -/
Concept.ofIsExtent : {α : Type u_2} → {β : Type u_3} → (r : α → β → Prop) → (s : Set α) → Order.IsExtent r s → Concept α β r
-- Mathlib.Analysis.Calculus.FDeriv.Norm
contDiffAt_norm_smul_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : WithTop ℕ∞} {x : E} {t : ℝ},
  t ≠ 0 → (ContDiffAt ℝ n (fun x => ‖x‖) x ↔ ContDiffAt ℝ n (fun x => ‖x‖) (t • x))
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_inj : ∀ {α : Type u_1} {a b : α}, SymAlg.sym a = SymAlg.sym b ↔ a = b
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOfMaxAdjoin.idealTo.eq_1 : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [inst_7 : Fact (Function.Injective ⇑i)] (y : N),
  Module.Baer.ExtensionOfMaxAdjoin.idealTo i f y =
    { toFun := fun z => ↑(Module.Baer.extensionOfMax i f).toLinearPMap ⟨↑z • y, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.State.hasSorry : Lean.Meta.Grind.Collector.State✝ → Bool
-- Std.Do.WP.Sound
/-- Soundness lemma for `ReaderM.run`: `Id`-specialization of `ReaderT.of_wp_run`.  -/
Std.Do.ReaderM.of_wp_run_eq : ∀ {α ρ : Type u} {x : α} {r : ρ} {prog : ReaderM ρ α},
  ReaderT.run prog r = x →
    ∀ (P : α → Prop), (⊢ₛ (Std.Do.wp prog).apply (Std.Do.PostCond.noThrow fun a x => ⌜P a⌝) r) → P x
-- Mathlib.Data.Finset.Powerset
/-- If two finsets of equal cardinality have the same `r`-element subsets for some `1 ≤ r ≤ #a`,
they are equal.  -/
Finset.eq_of_powersetCard_eq : ∀ {α : Type u_1} {a b : Finset α} {r : ℕ},
  a.card = b.card → r ≠ 0 → r ≤ a.card → Finset.powersetCard r a = Finset.powersetCard r b → a = b
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.instEpiPOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i],
  CategoryTheory.Epi (K.pOpcycles i)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.addConst.induct_unfolding : ∀ (k : ℤ) (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Prop),
  (∀ (k_1 : ℤ), motive (Int.Internal.Linear.Poly.num k_1) (Int.Internal.Linear.Poly.num (k + k_1))) →
    (∀ (k_1 : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
        motive p (p.addConst k) →
          motive (Int.Internal.Linear.Poly.add k_1 v p) (Int.Internal.Linear.Poly.add k_1 v (p.addConst k))) →
      ∀ (p : Int.Internal.Linear.Poly), motive p (p.addConst k)
-- Init.Prelude
Nat.lt_of_not_le : ∀ {a b : ℕ}, ¬a ≤ b → b < a
-- Mathlib.Topology.UniformSpace.UniformEmbedding
uniform_extend_subtype : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] [CompleteSpace γ] {p : α → Prop} {e : α → β} {f : α → γ} {b : β} {s : Set α},
  (UniformContinuous fun x => f ↑x) →
    IsUniformEmbedding e →
      (∀ (x : β), x ∈ closure (Set.range e)) →
        closure (e '' s) ∈ nhds b →
          IsClosed s → (∀ x ∈ s, p x) → ∃ c, Filter.Tendsto f (Filter.comap e (nhds b)) (nhds c)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.IsProbabilityMeasure.ne_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ], μ ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.mapAddMon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (hF : F.FullyFaithful),
  hF.mapAddMon =
    { preimage := fun {X Y} f => CategoryTheory.AddMon.Hom.mk' (hF.preimage f.hom) ⋯ ⋯, map_preimage := ⋯,
      preimage_map := ⋯ }
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.trace.inj : ∀ {cls : Lean.Name} {msg : Std.Format} {collapsed : Bool}
  {children : Lean.Widget.StrictOrLazy (Array Std.Format) (Array Lean.MessageData)} {cls_1 : Lean.Name}
  {msg_1 : Std.Format} {collapsed_1 : Bool}
  {children_1 : Lean.Widget.StrictOrLazy (Array Std.Format) (Array Lean.MessageData)},
  Lean.Widget.EmbedFmt.trace✝ cls msg collapsed children =
      Lean.Widget.EmbedFmt.trace✝ cls_1 msg_1 collapsed_1 children_1 →
    cls = cls_1 ∧ msg = msg_1 ∧ collapsed = collapsed_1 ∧ children = children_1
-- Init.Grind.Interactive
/-- `internalize` internalizes hypotheses into the grind E-graph.
Only available in `sym =>` mode.
- `internalize` internalizes the next hypothesis.
- `internalize <num>` internalizes the next `<num>` hypotheses.  -/
Lean.Parser.Tactic.Grind.symInternalize : Lean.ParserDescr
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_C : ∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], (Polynomial.C a).coeff n = if n = 0 then a else 0
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.inv₀` -/
TendstoLocallyUniformlyOn.fun_inv₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [inst_1 : TopologicalSpace X] {s : Set X}
  {F : ι → X → α} {f : X → α} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    ContinuousOn f s → (∀ x ∈ s, f x ≠ 0) → TendstoLocallyUniformlyOn (fun i i_1 => (F i i_1)⁻¹) (fun i => (f i)⁻¹) l s
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_ofNatLT : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatLT n hn).toBitVec = n#'hn
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.decomp_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Idempotents.Karoubi C),
  (CategoryTheory.Idempotents.toKaroubi C).map P.p = CategoryTheory.CategoryStruct.comp P.decompId_p P.decompId_i
-- Mathlib.Topology.Separation.Regular
Topology.IsEmbedding.t5Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T5Space Y] {e : X → Y},
  Topology.IsEmbedding e → T5Space X
-- Mathlib.RingTheory.Regular.RegularSequence
AddEquiv.isWeaklyRegular_congr : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] {e : M ≃+ M₂}
  {as : List R} {bs : List S},
  List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs →
    (RingTheory.Sequence.IsWeaklyRegular M as ↔ RingTheory.Sequence.IsWeaklyRegular M₂ bs)
-- Init.Data.SInt.Lemmas
Int8.zero_add : ∀ (a : Int8), 0 + a = a
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_X_sub_C_le : ∀ {R : Type u} [inst : Ring R] (r : R), (Polynomial.X - Polynomial.C r).natDegree ≤ 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.Const.get?.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : Option ((_ : α) × β) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (p : (_ : α) × β) → motive (some p)),
  (match none with
    | none => h_1 ()
    | some p => h_2 p) =
    h_1 ()
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.coe_codRestrict : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B] [inst_7 : StarRing B]
  [inst_8 : StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) (x : A),
  ↑((f.codRestrict S hf) x) = f x
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.comp.eq_4 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (_x _y _z : D) (f : (CategoryTheory.Join.right _x).Hom (CategoryTheory.Join.right _y))
  (g : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)),
  CategoryTheory.Join.comp f g = { down := CategoryTheory.CategoryStruct.comp f.down g.down }
-- Init.Data.String.Subslice
/-- Turns a subslice into a standalone slice by "forgetting" which slice the subslice is a sublice of.
 -/
String.Slice.Subslice.toSlice : {s : String.Slice} → s.Subslice → String.Slice
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (k : α), (t₁.insert k).Equiv (t₂.insert k)
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHomClass.toZeroHomClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : MulZeroOneClass α}
  {inst_1 : MulZeroOneClass β} {inst_2 : FunLike F α β} [self : MonoidWithZeroHomClass F α β], ZeroHomClass F α β
-- Std.Async.Process
Std.IO.Process.instOrdPId : Ord Std.IO.Process.PId
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.refl : Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.Geometry.Euclidean.Simplex
/-- The property of all angles of a simplex being acute.  -/
Affine.Simplex.AcuteAngled : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] → [inst_3 : NormedAddTorsor V P] → {n : ℕ} → Affine.Simplex ℝ P n → Prop
-- Mathlib.Topology.Semicontinuity.Lindelof
/-- If a function `s : X → E` can be written as the infimum of a family `𝓕` of upper semicontinuous
functions then, assuming that `X` is hereditarily Lindelöf (for example, second countable),
`s` can in fact be written as the infimum of some *countable* subfamily `𝓕'`.

This is implication a) ⇒ b) in
[N. Bourbaki, *Topologie Générale*, Chapitre IX, Appendice I, Proposition 3][bourbaki1974]

See the module docstring for a discussion of the assumptions on `E`.  -/
exists_countable_upperSemicontinuous_isGLB : ∀ {X : Type u_1} {E : Type u_2} [inst : TopologicalSpace X] [HereditarilyLindelofSpace X] [inst_2 : LinearOrder E]
  [inst_3 : TopologicalSpace E] [OrderClosedTopology E] [DenselyOrdered E] [TopologicalSpace.SeparableSpace E]
  {s : X → E} {𝓕 : Set (X → E)}, (∀ f ∈ 𝓕, UpperSemicontinuous f) → IsGLB 𝓕 s → ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ IsGLB 𝓕' s
-- Mathlib.Order.Category.HeytAlg
HeytAlg.hom_inv_apply : ∀ {X Y : HeytAlg} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.RingTheory.FinitePresentation
/-- An algebra morphism `A →ₐ[R] B` is of `AlgHom.FinitePresentation` if it is of finite
presentation as ring morphism. In other words, if `B` is finitely presented as `A`-algebra.  -/
AlgHom.FinitePresentation : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → Prop