mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
IsInertiaField.algebraMap_ringEquiv_apply : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (E : Type u_6) [inst_4 : Field E] [inst_5 : Algebra E L]
  [inst_6 : MulSemiringAction Gal(L/K) B] (E' : Type u_9) [inst_7 : Field E'] [inst_8 : Algebra E' L]
  [inst_9 : IsInertiaField K L P E] [inst_10 : IsInertiaField K L P E'] (x : E),
  (algebraMap E' L) ((IsInertiaField.ringEquiv K L P E E') x) = (algebraMap E L) x
-- Lean.Elab.ParseImportsFast
Lean.instToJsonPrintImportsResult.toJson : Lean.PrintImportsResult → Lean.Json
-- Lean.Data.Lsp.CodeActions
/-- The workspace edit this code action performs.  -/
Lean.Lsp.CodeAction.edit? : Lean.Lsp.CodeAction → Option Lean.Lsp.WorkspaceEdit
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.processLevel.go : Lean.Level → Lean.Level → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup'_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : SemilatticeSup β] (f : α → β), Finset.sup' 1 ⋯ f = f 1
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_div_left : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Div β] [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.IndepFun (f i / f j) (f k) μ
-- Mathlib.Analysis.Complex.ValueDistribution.Cartan
/-- The characteristic function is monotone on `(0, ∞)`. This result is surprisingly non-trivial, given
that the proximity function is not monotone in general.
 -/
ValueDistribution.characteristic_monotoneOn : ∀ {f : ℂ → ℂ}, Meromorphic f → MonotoneOn (ValueDistribution.characteristic f ⊤) (Set.Ioi 0)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- For a functor `F : C ⥤ D` and an object `d : D`, we obtain a contravariant functor from the
category of costructured arrows `F.op.obj c ⟶ op d` to the category of structured arrows
`d ⟶ F.obj c`.
 -/
CategoryTheory.CostructuredArrow.toStructuredArrow' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (d : D) →
            CategoryTheory.Functor (CategoryTheory.CostructuredArrow F.op (Opposite.op d))ᵒᵖ
              (CategoryTheory.StructuredArrow d F)
-- Std.Data.DHashMap.Internal.Model
/-- This is the general theorem to show that mapping operations (like `map` and `filter`) are
correct.  -/
Std.DHashMap.Internal.toListModel_updateAllBuckets : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Std.DHashMap.Internal.Raw₀ α β}
  {f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α δ}
  {g : List ((a : α) × β a) → List ((a : α) × δ a)},
  (∀ {l : Std.DHashMap.Internal.AssocList α β}, (f l).toList.Perm (g l.toList)) →
    (∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')) →
      (Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.updateAllBuckets (↑m).buckets f)).Perm
        (g (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- ProofWidgets.Component.RefreshComponent
/-- The index of the HTML tree that is currently on display.  -/
ProofWidgets.RefreshComponent.AwaitRefreshParams.oldIdx : ProofWidgets.RefreshComponent.AwaitRefreshParams → ℕ
-- Std.Tactic.Do.Syntax
/-- Like `rcases`, but operating on stateful `Std.Do.SPred` goals.
Example: Given a goal `h : (P ∧ (Q ∨ R) ∧ (Q → R)) ⊢ₛ R`,
`mcases h with ⟨-, ⟨hq | hr⟩, hqr⟩` will yield two goals:
`(hq : Q, hqr : Q → R) ⊢ₛ R` and `(hr : R) ⊢ₛ R`.

That is, `mcases h with pat` has the following semantics, based on `pat`:
* `pat=□h'` renames `h` to `h'` in the stateful context, regardless of whether `h` is pure
* `pat=⌜h'⌝` introduces `h' : φ`  to the pure local context if `h : ⌜φ⌝`
  (c.f. `Lean.Elab.Tactic.Do.ProofMode.IsPure`)
* `pat=h'` is like `pat=⌜h'⌝` if `h` is pure
  (c.f. `Lean.Elab.Tactic.Do.ProofMode.IsPure`), otherwise it is like `pat=□h'`.
* `pat=_` renames `h` to an inaccessible name
* `pat=-` discards `h`
* `⟨pat₁, pat₂⟩` matches on conjunctions and existential quantifiers and recurses via
  `pat₁` and `pat₂`.
* `⟨pat₁ | pat₂⟩` matches on disjunctions, matching the left alternative via `pat₁` and the right
  alternative via `pat₂`.
 -/
Lean.Parser.Tactic.mcases : Lean.ParserDescr
-- Mathlib.MeasureTheory.Order.Group.Lattice
measurable_negPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [inst_2 : MeasurableSpace α] [MeasurableNeg α]
  [MeasurableSup α], Measurable negPart
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.multisetProd_one : ∀ {n : ℕ} {s : Multiset ℕ}, (∀ x ∈ s, x ≡ 1 [MOD n]) → s.prod ≡ 1 [MOD n]
-- Lean.Parser.Term
Lean.Parser.Term.macroArg.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_insert_le_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k km kmi : α},
  t.min? = some km → (t.insert k).min?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.coe_toZFSet : ∀ {o : Ordinal.{u_1}}, ↑o.toZFSet = Ordinal.toZFSet '' Set.Iio o
-- Mathlib.Algebra.Lie.Submodule
/-- An injective morphism of Lie modules embeds the lattice of submodules of the domain into that
of the target.  -/
LieSubmodule.mapOrderEmbedding : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {M' : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : Module R M] →
                [inst_4 : LieRingModule L M] →
                  [inst_5 : AddCommGroup M'] →
                    [inst_6 : Module R M'] →
                      [inst_7 : LieRingModule L M'] →
                        {f : M →ₗ⁅R,L⁆ M'} → Function.Injective ⇑f → LieSubmodule R L M ↪o LieSubmodule R L M'
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
_private.Mathlib.MeasureTheory.Integral.Lebesgue.Basic.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.instIsCocontinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).IsCocontinuous (Opens.grothendieckTopology ↥X)
    (Opens.grothendieckTopology ↥Y)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.natCast_mul_le_natCast_mul : ∀ {n : ℕ} {a b : Cardinal.{u_1}}, n ≠ 0 → (↑n * a ≤ ↑n * b ↔ a ≤ b)
-- Init.Data.String.Basic
String.Pos.Raw.isValid_eq_false_iff : ∀ {s : String} {p : String.Pos.Raw}, String.Pos.Raw.isValid s p = false ↔ ¬String.Pos.Raw.IsValid s p
-- Mathlib.Data.Set.Finite.Lattice
/-- A decreasing intersection distributes over finite union.  -/
Set.iInter_iUnion_of_antitone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [IsDirectedOrder ι'] [Nonempty ι']
  {s : ι → ι' → Set α}, (∀ (i : ι), Antitone (s i)) → ⋂ j, ⋃ i, s i j = ⋃ i, ⋂ j, s i j
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instDistrib : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Distrib Y] → Distrib (LocallyConstant X Y)
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.toQuotientPaths_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.toQuotientPaths C).map f =
    Quot.mk (CategoryTheory.HomRel.CompClosure (CategoryTheory.pathsHomRel C)) f.toPath
-- Mathlib.Topology.Order.DenselyOrdered
frontier_Iic : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMaxOrder α] {a : α}, frontier (Set.Iic a) = {a}
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Swapping the last two points preserves affine independence.  -/
AffineIndependent.comm_right : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P}, AffineIndependent k ![p₁, p₂, p₃] → AffineIndependent k ![p₁, p₃, p₂]
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- compatibility condition  -/
CategoryTheory.Endofunctor.Coalgebra.Hom.h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (self : V₀.Hom V₁),
  CategoryTheory.CategoryStruct.comp V₀.str (F.map self.f) = CategoryTheory.CategoryStruct.comp self.f V₁.str
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.mapSnakeInput_f₀ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂)
  (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j),
  (HomologicalComplex.HomologySequence.mapSnakeInput φ hS₁ hS₂ i j hij).f₀ =
    (HomologicalComplex.homologyFunctor C c i).mapShortComplex.map φ
-- Init.Data.UInt.Basic
instOrOpUInt64 : OrOp UInt64
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.paramNames : Lean.Meta.AbstractMVars.State → Array Lean.Name
-- Lean.Meta.Tactic.Grind.ProveEq
/-- Number of binders under which the terms being processed occur under.  -/
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.Context.offset : Lean.Meta.Grind.AbstractM.Context✝ → ℕ
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
/-- Define a right action of `C` on `D` from a right action of `Cᵒᵖ` on `Dᵒᵖ` via
the formula `d ⊙ᵣ c = unop ((op d) ⊙ᵣ (op c))`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ] →
            CategoryTheory.MonoidalCategory.MonoidalRightAction C D
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.chainsIso₂.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.chainsIso₂ A = (Finsupp.domLCongr (piFinTwoEquiv fun x => G)).toModuleIso
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.coe_toAffineMap : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂), ⇑f.toAffineMap = ⇑f
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.circumcenterWeightsWithCircumcenter.eq_2 : ∀ (n : ℕ),
  Affine.Simplex.circumcenterWeightsWithCircumcenter n Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex = 1
-- Init.Data.UInt.Bitwise
UInt64.ne_not_self : ∀ {a : UInt64}, a ≠ ~~~a
-- Lean.Server.References
/-- URI of the module that the file worker is associated with.  -/
Lean.Server.TransientWorkerILean.moduleUri : Lean.Server.TransientWorkerILean → Lean.Lsp.DocumentUri
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.instHtmlEvalCoreMHtml : ProofWidgets.HtmlEval (Lean.CoreM ProofWidgets.Html)
-- Mathlib.Order.SupClosed
compl_image_latticeClosure_eq_of_compl_image_eq_self : ∀ {α : Type u_3} [inst : BooleanAlgebra α] {s : Set α}, compl '' s = s → compl '' latticeClosure s = latticeClosure s
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyRel.compContinuousMap_apply : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {S : Set X} {f₀ f₁ : C(X, Y)} (F : f₀.HomotopyRel f₁ S) (g : C(Y, Z))
  (x : ↑unitInterval × X), (F.compContinuousMap g) x = g (F x)
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.Prepartition.toSubordinate_toPrepartition_le : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (r : (ι → ℝ) → ↑(Set.Ioi 0)), (π.toSubordinate r).toPrepartition ≤ π
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.gcd_dvd : ∀ {x y z : ℤ}, PythagoreanTriple x y z → ↑(x.gcd y) ∣ z
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- A morphism `f : Y ⟶ X` is an effective epimorphism provided that `f` exhibits `X` as a colimit
of the diagram of all "relations" `R ⇉ Y`.
If `f` has a kernel pair, then this is equivalent to showing that the corresponding cofork is
a colimit.
 -/
CategoryTheory.EffectiveEpi : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {X Y : C} → (Y ⟶ X) → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAt.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},
  HasFDerivAt f f' x →
    Topology.IsInducing ⇑f' → Asymptotics.IsEquivalent (nhds x) (fun x_1 => f x_1 - f x) fun x_1 => f' (x_1 - x)
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- A CW complex that was constructed using `RelCWComplex.mkFinite` is finite.  -/
Topology.RelCWComplex.finite_mkFinite : ∀ {X : Type u} [inst : TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : ℕ → Type u)
  (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X)
  (eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)) (finite_cell : ∀ (n : ℕ), Finite (cell n))
  (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1)
  (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1))
  (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target)
  (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1)
  (disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' Metric.ball 0 1) D)
  (mapsTo :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1))
  (isClosedBase : IsClosed D) (union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C),
  Topology.RelCWComplex.Finite C
-- Mathlib.Data.Fin.SuccPred
Fin.castPred.eq_1 : ∀ {n : ℕ} (i : Fin (n + 1)) (h : i ≠ Fin.last n), i.castPred h = i.castLT ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_add_eq_sub_pi : ∀ {x y : ℝ}, 1 < x * y → x < 0 → Real.arctan x + Real.arctan y = Real.arctan ((x + y) / (1 - x * y)) - Real.pi
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIci.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α),
  Set.instFintypeIci a = Fintype.ofFinset (Finset.Ici a) ⋯
-- Mathlib.Analysis.Convex.Body
/-- Let `V` be a real topological vector space. A subset of `V` is a convex body if and only if
it is convex, compact, and nonempty.
 -/
ConvexBody : (V : Type u_2) → [TopologicalSpace V] → [AddCommMonoid V] → [SMul ℝ V] → Type u_2
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.addSingleEquiv.eq_1 : ∀ {R : Type u_4} {ι : Type u_6} [inst : Ring R] (i : ι) (c : ι → R) (h₀ : c i = 0),
  Finsupp.addSingleEquiv i c h₀ =
    LinearEquiv.ofLinearMap (Finsupp.linearCombination R fun j => (fun₀ | j => 1) + fun₀ | i => c j)
      (Finsupp.linearCombination R fun j => (fun₀ | j => 1) - fun₀ | i => c j) ⋯ ⋯
-- Mathlib.Tactic.Linter.TextBased
/-- The line number of the error (1-based)  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ErrorContext.lineNumber : Mathlib.Linter.TextBased.ErrorContext✝ → ℕ
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.mk_eq_top : ∀ {M : Type u_1} [inst : Add M] (carrier : Set M) (add_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier),
  { carrier := carrier, add_mem' := add_mem' } = ⊤ ↔ carrier = Set.univ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, k ∈ m₂ → (m₁ ∩ m₂).getKey! k = m₁.getKey! k
-- Mathlib.GroupTheory.SemidirectProduct
/-- The isomorphism from a semidirect product of complementary subgroups to the ambient group.  -/
SemidirectProduct.mulEquivSubgroup : {G : Type u_2} →
  [inst : Group G] →
    {H K : Subgroup G} →
      [inst_1 : H.Normal] → H.IsComplement' K → ↥H ⋊[H.normalizerMonoidHom.comp (Subgroup.inclusion ⋯)] ↥K ≃* G
-- Lean.KeyedDeclsAttribute
/-- Retrieve values tagged with `[attr key]` or `[builtinAttr key]`.  -/
Lean.KeyedDeclsAttribute.getValues : {γ : Type} → Lean.KeyedDeclsAttribute γ → Lean.Environment → Lean.Name → List γ
-- Mathlib.Data.Finset.Pi
Finset.pi_eq_empty : ∀ {α : Type u_1} {β : α → Type u} {s : Finset α} {t : (a : α) → Finset (β a)} [inst : DecidableEq α],
  s.pi t = ∅ ↔ ∃ a ∈ s, t a = ∅
-- Lean.Meta.Transform
/-- Unfold definitions and theorems in `e` that are not in the current environment, but are in `biggerEnv`.  -/
Lean.Meta.unfoldDeclsFrom : Lean.Environment → Lean.Expr → Lean.CoreM Lean.Expr
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof : Type
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normNatPowInst : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.List.Destutter
List.destutter_pair : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {a b : α},
  List.destutter R [a, b] = if R a b then [a, b] else [a]
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_le_cos_of_nonneg_of_le_pi : ∀ {x y : ℝ}, 0 ≤ x → y ≤ Real.pi → x ≤ y → Real.cos y ≤ Real.cos x
-- Mathlib.GroupTheory.Exponent
AddMonoid.ExponentExists.eq_1 : ∀ (G : Type u) [inst : AddMonoid G], AddMonoid.ExponentExists G = ∃ n, 0 < n ∧ ∀ (g : G), n • g = 0
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.coe_mapAlgHom_eq_coe_map : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {R : Type u_2} {S : Type u_3} [inst_2 : CommRing R]
  [inst_3 : IsDomain R] [inst_4 : CommSemiring S] [inst_5 : Algebra S (Polynomial K)]
  [inst_6 : Algebra S (Polynomial R)] (φ : Polynomial K →ₐ[S] Polynomial R)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))),
  ⇑(RatFunc.mapAlgHom φ hφ) = ⇑(RatFunc.map φ hφ)
-- Batteries.Tactic.OpenPrivate
/-- Core elaborator for `open private` and `export private`.  -/
Lean.Elab.Command.elabOpenPrivateLike : Array Lean.Ident →
  Option (Array Lean.Ident) →
    Option (Array Lean.Ident) →
      (Lean.Name → Lean.Name → Lean.Name → Lean.Elab.Command.CommandElabM Lean.Name) →
        Lean.Elab.Command.CommandElabM Unit
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
/-- Given an exact sequence of `G`-representations `0 ⟶ X₁ ⟶f X₂ ⟶g X₃ ⟶ 0`, this expresses an
`n + 1`-cochain `x : Gⁿ⁺¹ → X₁` such that `f ∘ x ∈ Bⁿ⁺¹(G, X₂)` as a cocycle.
Stated for readability of `δ_apply`.  -/
groupCohomology.cocyclesMkOfCompEqD : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} →
        X.ShortExact →
          {i j : ℕ} →
            {y : (Fin i → G) → ↑X.X₂} →
              {x : (Fin j → G) → ↑X.X₁} →
                ⇑(Rep.Hom.hom X.f) ∘ x =
                    (CategoryTheory.ConcreteCategory.hom ((groupCohomology.inhomogeneousCochains X.X₂).d i j)) y →
                  ↑(groupCohomology.cocycles X.X₁ j)
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.δ₀Iter_succ'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (h : autoParam (n + (i + 1) = m) CategoryTheory.SimplicialObject.δ₀Iter_succ'._auto_1) {Z : C}
  (h_1 : X.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ₀Iter (i + 1) h) h_1 =
    CategoryTheory.CategoryStruct.comp (X.δ₀Iter i ⋯) (CategoryTheory.CategoryStruct.comp (X.δ 0) h_1)
-- Aesop.Util.Basic
/-- Remove elements for which `p` returns `false` from the given `DiscrTree`.
The removed elements are folded over using `f` and `init`, so `f` is called
once for each removed element and the final state of type `σ` is returned.
 -/
Aesop.filterDiscrTree : {σ : Type u_1} →
  {α : Type} → [Inhabited σ] → (α → Bool) → (σ → α → σ) → σ → Lean.Meta.DiscrTree α → Lean.Meta.DiscrTree α × σ
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.sub_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s t : Set α},
  IsLowerSet s → IsLowerSet (s - t)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.Adjunction.toCokleisli_map_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) {X x : C} (f : X ⟶ x),
  ((CategoryTheory.Cokleisli.Adjunction.toCokleisli U).map f).of = CategoryTheory.CategoryStruct.comp (U.ε.app X) f
-- Mathlib.Topology.Filter
Filter.nhds_inf : ∀ {α : Type u_2} (l₁ l₂ : Filter α), nhds (l₁ ⊓ l₂) = nhds l₁ ⊓ nhds l₂
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.diagram : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {j k : J} → (j ⟶ k) → CategoryTheory.BiconeHom J (CategoryTheory.Bicone.diagram j) (CategoryTheory.Bicone.diagram k)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.pair_sdiff_left`. -/
Set.pair_diff_left : ∀ {α : Type u_1} {a b : α}, a ≠ b → {a, b} \ {a} = {b}
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The affine open sets of an open subscheme corresponds to
the affine open sets containing in the image.  -/
AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [H : AlgebraicGeometry.IsOpenImmersion f] →
      ↑X.affineOpens ≃o { U // ↑U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f }
-- Mathlib.Data.Set.Lattice.Image
Set.iInter₂_union_iInter₂ : ∀ {α : Type u_1} {ι₁ : Sort u_9} {κ₁ : Sort u_10} {ι₂ : ι₁ → Sort u_11} {k₂ : κ₁ → Sort u_12}
  (f : (i₁ : ι₁) → ι₂ i₁ → Set α) (g : (j₁ : κ₁) → k₂ j₁ → Set α),
  (⋂ i₁, ⋂ i₂, f i₁ i₂) ∪ ⋂ j₁, ⋂ j₂, g j₁ j₂ = ⋂ i₁, ⋂ i₂, ⋂ j₁, ⋂ j₂, f i₁ i₂ ∪ g j₁ j₂
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.map_coeff : ∀ {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero S]
  (x : HahnSeries Γ R) {F : Type u_5} [inst_3 : FunLike F R S] [inst_4 : ZeroHomClass F R S] (f : F) (g : Γ),
  (x.map f).coeff g = f (x.coeff g)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.contradiction_of_insertUnit_success : ∀ {n : ℕ} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n)
  (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (foundContradiction : Bool)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  let insertUnit_res :=
    Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l;
  (foundContradiction = true → ∃ i, assignments[↑i] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both) →
    insertUnit_res.2.2 = true → ∃ j, insertUnit_res.2.1[↑j] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.zip.eq_1 : ∀ {α : Type u} {β : Type u_1} (as : Array α) (bs : Array β), as.zip bs = Array.zipWith Prod.mk as bs
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_div_Ioi : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a / x) '' Set.Ioi b = Set.Iio (a / b)