mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C)
  [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois A] (a : (F.obj A).obj),
  CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A a =
    Equiv.ofBijective (fun f => (CategoryTheory.ConcreteCategory.hom (F.map f.hom)) a) ⋯
-- Mathlib.RingTheory.NoetherNormalization
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.leadingCoeff_finSuccEquiv_t : ∀ {k : Type u_1} [inst : Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (v : Fin (n + 1) →₀ ℕ),
  ((MvPolynomial.finSuccEquiv k n)
        ((NoetherNormalization.T✝ f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- The isomorphism between an object and its normal form is natural.  -/
CategoryTheory.FreeMonoidalCategory.fullNormalizeIso : (C : Type u) →
  CategoryTheory.Functor.id (CategoryTheory.FreeMonoidalCategory C) ≅
    (CategoryTheory.FreeMonoidalCategory.fullNormalize C).comp CategoryTheory.FreeMonoidalCategory.inclusion
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β] (f : InfTopHom α β)
  (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.CategoryTheory.Sites.Continuous
/-- A functor `F` is continuous if the precomposition with `F.op` sends sheaves of
`Type (max u₁ v₁ u₂ v₂)` to sheaves. This implies that this holds for an arbitrary
universe (see `Functor.op_comp_isSheaf_of_types`).  -/
CategoryTheory.Functor.IsContinuous : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.GrothendieckTopology C → CategoryTheory.GrothendieckTopology D → Prop
-- Mathlib.Data.Fintype.Inv
Fintype.choose_spec : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p] (hp : ∃! a, p a), p (Fintype.choose p hp)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.iSup_ofHoms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type u_3} {ι : α → Type u_4} {A B : (a : α) → ι a → C}
  (f : (a : α) → (i : ι a) → A a i ⟶ B a i),
  ⨆ a, CategoryTheory.MorphismProperty.ofHoms (f a) = CategoryTheory.MorphismProperty.ofHoms fun j => f j.fst j.snd
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.le_ind : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C), P ≤ P.ind
-- Init.Data.AC
Lean.Data.AC.Expr.toList.eq_def : ∀ (x : Lean.Data.AC.Expr),
  x.toList =
    match x with
    | Lean.Data.AC.Expr.var idx => [idx]
    | l.op r => l.toList.append r.toList
-- Mathlib.Data.Seq.Computation
Computation.orElse_empty : ∀ {α : Type u} (c : Computation α), (c <|> Computation.empty α) = c
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- The object in the original category indexed by `x : I`.  -/
CategoryTheory.Limits.FormalCoproduct.obj : {C : Type u} → (self : CategoryTheory.Limits.FormalCoproduct C) → self.I → C
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure_C_mul_X_add_C : ∀ {a : ℂ},
  a ≠ 0 → ∀ (b : ℂ), (Polynomial.C a * Polynomial.X + Polynomial.C b).logMahlerMeasure = Real.log ‖a‖ + ‖a⁻¹ * b‖.posLog
-- Mathlib.RingTheory.KrullDimension.NonZeroDivisors
ringKrullDim_succ_le_ringKrullDim_polynomial : ∀ {R : Type u_1} [inst : CommRing R], ringKrullDim R + 1 ≤ ringKrullDim (Polynomial R)
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Build an `AddEquiv` from an isomorphism in the category
`AddCommMonCat`.  -/
CategoryTheory.Iso.commMonCatIsoToAddEquiv : {X Y : AddCommMonCat} → (X ≅ Y) → ↑X ≃+ ↑Y
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- **Alias** of `MonoidAlgebra.coeff_domCongr`. -/
MonoidAlgebra.domCongr_apply : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (e : M ≃* N) (f : MonoidAlgebra A M) (n : N),
  ((MonoidAlgebra.domCongr R A e) f).coeff n = f.coeff (e.symm n)
-- Mathlib.Data.Set.Lattice.Image
Set.image2_sInter_left_subset : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (S : Set (Set α)) (t : Set β) (f : α → β → γ),
  Set.image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, Set.image2 f s t
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instHasDistribNeg : HasDistribNeg Complex.UnitDisc
-- Mathlib.Algebra.MvPolynomial.Eval
/-- `MvPolynomial.eval₂ (algebraMap R S) g` as an `R`-algebra homomorphism.  -/
MvPolynomial.eval₂AlgHom : (R : Type u) →
  {S₁ : Type v} →
    {σ : Type u_1} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S₁] → [inst_2 : Algebra R S₁] → (σ → S₁) → MvPolynomial σ R →ₐ[R] S₁
-- Lean.Elab.Syntax
Lean.Elab.Command.isLocalAttrKind : Lean.Syntax → Bool
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- The canonical `algEquiv` between `K⟮x⟯` and `K⟮y⟯`, sending `x` to `y`, where `x` and `y` have
the same minimal polynomial over `K`.  -/
minpoly.algEquiv : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → {x y : L} → IsAlgebraic K x → minpoly K x = minpoly K y → ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- If the image under the seminorm is zero, then the argument is zero.  -/
MulRingNorm.eq_zero_of_map_eq_zero' : ∀ {R : Type u_2} [inst : NonAssocRing R] (self : MulRingNorm R) (x : R), self.toFun x = 0 → x = 0
-- Mathlib.Data.Quot
/-- Given a function `f : Π i, Quotient (S i)`, returns the class of functions `Π i, α i` sending
each `i` to an element of the class `f i`.  -/
Quotient.choice : {ι : Type u_3} → {α : ι → Type u_4} → {S : (i : ι) → Setoid (α i)} → ((i : ι) → Quotient (S i)) → Quotient inferInstance
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolAux.mk.inj : ∀ {Self : Type} {name : String} {detail? : Option String} {kind : Lean.Lsp.SymbolKind}
  {range selectionRange : Lean.Lsp.Range} {children? : Option (Array Self)} {name_1 : String}
  {detail?_1 : Option String} {kind_1 : Lean.Lsp.SymbolKind} {range_1 selectionRange_1 : Lean.Lsp.Range}
  {children?_1 : Option (Array Self)},
  { name := name, detail? := detail?, kind := kind, range := range, selectionRange := selectionRange,
        children? := children? } =
      { name := name_1, detail? := detail?_1, kind := kind_1, range := range_1, selectionRange := selectionRange_1,
        children? := children?_1 } →
    name = name_1 ∧
      detail? = detail?_1 ∧
        kind = kind_1 ∧ range = range_1 ∧ selectionRange = selectionRange_1 ∧ children? = children?_1
-- Mathlib.FieldTheory.FinTrdeg
finite_of_isTranscendenceBasis : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FinTrdeg K L] {ι : Type u_3}
  {x : ι → L}, IsTranscendenceBasis K x → Finite ι
-- Mathlib.Topology.UniformSpace.Basic
IsClosed.relInv : ∀ {α : Type ua} {β : Type ub} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : SetRel α β},
  IsClosed s → IsClosed s.inv
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- The rotation by 90 degrees on an oriented real inner product space of dimension 2 can be
evaluated in terms of a complex-number representation of the space.  -/
Orientation.rightAngleRotation_map_complex : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (f : E ≃ₗᵢ[ℝ] ℂ),
  (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation →
    ∀ (x : E), f (o.rightAngleRotation x) = Complex.I * f x
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `<*>`, weakest precondition version 1.
(Use this when `x` and the goal are known and `f` is a subgoal.)
 -/
SatisfiesM.seq_pre : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p₂ : α → Prop} {α_1 : Type u_1} {q : α_1 → Prop} {f : m (α → α_1)}
  [inst : Applicative m] [LawfulApplicative m] {x : m α},
  SatisfiesM (fun f => ∀ {a : α}, p₂ a → q (f a)) f → SatisfiesM p₂ x → SatisfiesM q (f <*> x)
-- Mathlib.Tactic.Push
/-- `push_neg` rewrites the goal by pushing negations deeper into an expression.
For instance, the goal `¬ ∀ x, ∃ y, x ≤ y` will be transformed by `push_neg` into
`∃ x, ∀ y, y < x`. Binder names are preserved (contrary to what would happen with `simp`
using the relevant lemmas). `push_neg` works as both a tactic and a conv tactic.

`push_neg` is a special case of the more general `push` tactic, namely `push Not`.
The `push` tactic can be extended using the `@[push]` attribute. `push` has special-casing
built in for `push Not`.

Tactics that introduce a negation usually have a version that automatically calls `push_neg` on
that negation. These include `by_cases!`, `contrapose!` and `by_contra!`.

* `push_neg at l1 l2 ...` rewrites at the given locations.
* `push_neg at *` rewrites at each hypothesis and the goal.
* `push_neg +distrib` rewrites `¬ (p ∧ q)` into `¬ p ∨ ¬ q` (by default, the tactic rewrites it
  into `p → ¬ q` instead).

Example:

```lean
example (h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε) :
    ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀| := by
  push_neg at h
  -- Now we have the hypothesis `h : ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|`
  exact h
```
 -/
Mathlib.Tactic.Push.convPush_neg_ : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Module.Span
ContinuousLinearEquiv.toSpanNonzeroSingleton_coord : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {x : E} (h : x ≠ 0) (y : ↥(𝕜 ∙ x)),
  (ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h) ((ContinuousLinearEquiv.coord 𝕜 x h) y) = y
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.zero_add : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
SeparationQuotient.apply_eq_apply_of_inseparable : ∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N] {F : Type u_3}
  [inst_2 : FunLike F M N] [AddMonoidHomClass F M N] (f : F),
  (∀ (x : M), ‖x‖ = 0 → f x = 0) → ∀ (x y : M), Inseparable x y → f x = f y
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_ball' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.ball x ε ↔ dist x y < ε
-- Init.Data.List.Nat.TakeDrop
List.take_reverse : ∀ {α : Type u_1} {xs : List α} {i : ℕ}, List.take i xs.reverse = (List.drop (xs.length - i) xs).reverse
-- Init.NotationExtra
«term_×'__1» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Category.TwoP
pointedToTwoPFst_comp_forget_to_bipointed : pointedToTwoPFst.comp (CategoryTheory.forget₂ TwoP Bipointed) = pointedToBipointedFst
-- Init.Data.List.BasicAux
List.not_lex_antisymm : ∀ {α : Type u_1} [DecidableEq α] {r : α → α → Prop} [DecidableRel r],
  (∀ (x y : α), ¬r x y → ¬r y x → x = y) → ∀ {as bs : List α}, ¬List.Lex r bs as → ¬List.Lex r as bs → as = bs
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.inter_eq_of_subset_indep : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis I X → I ⊆ J → M.Indep J → J ∩ X = I
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd : {α : outParam (Type u)} →
  {β : outParam (Type v)} →
    {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} →
      {σ : Type w} →
        {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} →
          [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] → σ → β → Array ℕ → σ × Bool
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.struct.inj : ∀ {leanTypeName : Option Lean.Name} {types : Array Lean.IR.IRType} {leanTypeName_1 : Option Lean.Name}
  {types_1 : Array Lean.IR.IRType},
  Lean.IR.IRType.struct leanTypeName types = Lean.IR.IRType.struct leanTypeName_1 types_1 →
    leanTypeName = leanTypeName_1 ∧ types = types_1
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) (AlgebraicGeometry.SheafedSpace.forget C)
-- Init.Data.List.Erase
List.mem_erase_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {l : List α}, a ≠ b → (a ∈ l.erase b ↔ a ∈ l)
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.fun_comp : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {N : Type u_3} [inst_1 : One N] {g : M → N} {f : α → M},
  Function.HasFiniteMulSupport f → g 1 = 1 → Function.HasFiniteMulSupport fun a => g (f a)
-- Init.Data.Vector.Lemmas
Vector.mem_of_getElem? : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {a : α}, xs[i]? = some a → a ∈ xs
-- Mathlib.Order.RelClasses
isStrictWeakOrder_of_isOrderConnected : ∀ {α : Type u} {r : α → α → Prop} [Std.Asymm r] [IsOrderConnected α r], IsStrictWeakOrder α r
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The homology isomorphism `S₁.homology ⟶ S₂.homology` induced by an isomorphism
`S₁ ≅ S₂` of short complexes.  -/
CategoryTheory.ShortComplex.homologyMapIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ≅ S₂) → [inst_2 : S₁.HasHomology] → [inst_3 : S₂.HasHomology] → S₁.homology ≅ S₂.homology
-- Lean.Util.Trace
Lean.MonadAlwaysExcept.except : {ε : outParam (Type u)} → {m : Type u → Type v} → [self : Lean.MonadAlwaysExcept ε m] → MonadExceptOf ε m
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.mfderivWithin_eq_zero : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  HasMFDerivAt[s] f x 0 → mfderiv[s] f x = 0
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.unit_app_ev_app_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F H]
  (ℌ : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) (x y : C) {Z : V}
  (h : G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F H).app (x, y))
      (CategoryTheory.CategoryStruct.comp (ℌ.ev_app.app (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry (ℌ.π y x)) h
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.lift_zero : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃), q.lift 0 = 0
-- Mathlib.Geometry.Euclidean.Volume.Measure
MeasureTheory.euclideanHausdorffMeasure_homothety_image : ∀ {𝕜 : Type u_3} {V : Type u_4} {P : Type u_5} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : MeasurableSpace P] [inst_4 : MetricSpace P] [inst_5 : NormedAddTorsor V P]
  [inst_6 : BorelSpace P] (d : ℕ) (x : P) {c : 𝕜},
  c ≠ 0 →
    ∀ (s : Set P),
      (MeasureTheory.Measure.euclideanHausdorffMeasure d) (⇑(AffineMap.homothety x c) '' s) =
        ‖c‖₊ ^ d • (MeasureTheory.Measure.euclideanHausdorffMeasure d) s
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
TopCat.Presheaf.IsSheafUniqueGluing.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X : TopCat}
  (F : TopCat.Presheaf C X),
  F.IsSheafUniqueGluing =
    ∀ ⦃ι : Type x⦄ (U : ι → TopologicalSpace.Opens ↑X)
      (sf : (i : ι) → CategoryTheory.ToType (F.obj (Opposite.op (U i)))), F.IsCompatible U sf → ∃! s, F.IsGluing U sf s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ {k : α}, (Std.DTreeMap.Internal.Impl.erase! k t₁).Equiv (Std.DTreeMap.Internal.Impl.erase! k t₂)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
OpenPartialHomeomorph.Simps.apply : {X : Type u_1} →
  {Y : Type u_3} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → OpenPartialHomeomorph X Y → X → Y
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
instNonemptySubtypeSetAlgebraicIndepOnIdOfFaithfulSMul : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [FaithfulSMul R A],
  Nonempty { s // AlgebraicIndepOn R id s }
-- Mathlib.Data.List.Lattice
List.inter_cons : ∀ {α : Type u_1} {l₂ : List α} {a : α} [inst : DecidableEq α] (l₁ : List α),
  (a :: l₁) ∩ l₂ = if a ∈ l₂ then a :: l₁ ∩ l₂ else l₁ ∩ l₂
-- Init.Data.Vector.Lemmas
Vector.findSomeRevM?_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] {f : α → m (Option β)}
  {xs : Vector α n}, Array.findSomeRevM? f xs.toArray = Vector.findSomeRevM? f xs
-- Mathlib.Topology.Category.LightProfinite.Basic
LightDiagram'.mk.injEq : ∀ (diagram diagram_1 : CategoryTheory.Functor ℕᵒᵖ FintypeCat.Skeleton),
  ({ diagram := diagram } = { diagram := diagram_1 }) = (diagram = diagram_1)
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.instModuleNNRat : {M : Type u_1} → [inst : AddCommMonoid M] → Module ℚ≥0 (DivisibleHull M)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.add_vadd : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (x y : AddOreLocalization S R) (z : AddOreLocalization S X), (x + y) +ᵥ z = x +ᵥ y +ᵥ z
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The category of semigroups and semigroup morphisms.  -/
Semigrp : Type (u + 1)
-- Mathlib.Data.Set.NAry
Set.Subsingleton.image2 : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {s : Set α} {t : Set β},
  s.Subsingleton → t.Subsingleton → ∀ (f : α → β → γ), (Set.image2 f s t).Subsingleton
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_eq_zero_iff : ∀ {E : Type u_5} [inst : NormedAddGroup E] {a b : E}, ‖a - b‖ = 0 ↔ a = b
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.ext_get?_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {m₁ m₂ : Std.ExtHashSet α}, m₁ = m₂ ↔ ∀ (k : α), m₁.get? k = m₂.get? k
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.sproj.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (n offset : ℕ) (var : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_11) (n_1 offset_1 : ℕ)
  (var_1 : Lean.FVarId) (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_11),
  (Lean.Compiler.LCNF.LetValue.sproj n offset var h = Lean.Compiler.LCNF.LetValue.sproj n_1 offset_1 var_1 h_1) =
    (n = n_1 ∧ offset = offset_1 ∧ var = var_1)
-- Mathlib.RingTheory.Spectrum.Maximal.Defs
instCoeMaximalSpectrumIdeal : (R : Type u_1) → [inst : CommSemiring R] → Coe (MaximalSpectrum R) (Ideal R)
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
groupAddGroupEquivalence_functor : groupAddGroupEquivalence.functor = GrpCat.toAddGrp
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Φ_coeff_generatorIndex : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  (algebraMap (Polynomial K) (RatFunc K)) ((RatFunc.Luroth.Φ✝ E).coeff (RatFunc.Luroth.generatorIndex✝ h)) =
    (algebraMap (Polynomial K) (RatFunc K)) (RatFunc.Luroth.c✝ E).num * RatFunc.Luroth.generator E
-- Mathlib.Control.LawfulFix
Pi.monotoneCurry_coe : ∀ (α : Type u_1) (β : α → Type u_2) (γ : (a : α) → β a → Type u_3) [inst : (x : α) → (y : β x) → Preorder (γ x y)]
  (f : (x : (a : α) × β a) → γ x.fst x.snd) (x : α) (y : β x), (Pi.monotoneCurry α β γ) f x y = Sigma.curry f x y
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.eval.match_1.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {K : CategoryTheory.Precoverage C}
  (ι : C → Type (max u_1 u_2))
  (motive : (x : C) → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι x → Sort u_3) (X : C) (i : ι X)
  (h_1 : (X : C) → (i : ι X) → motive X (CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ X i))
  (h_2 :
    (x Y : C) →
      (f : x ⟶ Y) →
        (i : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι Y) →
          motive x (CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f i))
  (h_3 :
    (x : C) →
      (R : CategoryTheory.Presieve x) →
        (hR : R ∈ K.coverings x) →
          (h : ⦃W : C⦄ → (r : W ⟶ x) → R r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W) →
            motive x (CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h)),
  (match X, CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ X i with
    | X, CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ .(X) i => h_1 X i
    | x, CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f i => h_2 x Y f i
    | x, CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h => h_3 x R hR h) =
    h_1 X i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.le_maxKey!_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {k : α}, k ∈ t → (compare k t.maxKey!).isLE = true
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
isLocalHom_of_exists_map_ne_one : ∀ {M : Type u_1} {G₀ : Type u_3} {F : Type u_6} [inst : Monoid M] [inst_1 : GroupWithZero G₀] [inst_2 : FunLike F G₀ M]
  [MonoidHomClass F G₀ M] {f : F}, (∃ x, f x ≠ 1) → IsLocalHom f
-- Mathlib.Condensed.Explicit
/-- The condensed object associated to a presheaf on `CompHaus` which preserves finite products and
satisfies the equalizer condition.
 -/
Condensed.ofSheafCompHaus : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    (F : CategoryTheory.Functor CompHausᵒᵖ A) →
      [CategoryTheory.Limits.PreservesFiniteProducts F] →
        CategoryTheory.regularTopology.EqualizerCondition F → Condensed A
-- Mathlib.GroupTheory.OrderOfElement
zpow_mod_card : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] (a : G) (n : ℤ), a ^ (n % ↑(Fintype.card G)) = a ^ n