mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.mk.inj : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} {inst : TopologicalSpace B} {inst_1 : TopologicalSpace F}
  {inst_2 : TopologicalSpace Z} {proj : Z → B} {toOpenPartialHomeomorph : OpenPartialHomeomorph Z (B × F)}
  {baseSet : Set B} {open_baseSet : IsOpen baseSet} {source_eq : toOpenPartialHomeomorph.source = proj ⁻¹' baseSet}
  {target_eq : toOpenPartialHomeomorph.target = baseSet ×ˢ Set.univ}
  {proj_toFun : ∀ p ∈ toOpenPartialHomeomorph.source, (↑toOpenPartialHomeomorph p).1 = proj p}
  {toOpenPartialHomeomorph_1 : OpenPartialHomeomorph Z (B × F)} {baseSet_1 : Set B} {open_baseSet_1 : IsOpen baseSet_1}
  {source_eq_1 : toOpenPartialHomeomorph_1.source = proj ⁻¹' baseSet_1}
  {target_eq_1 : toOpenPartialHomeomorph_1.target = baseSet_1 ×ˢ Set.univ}
  {proj_toFun_1 : ∀ p ∈ toOpenPartialHomeomorph_1.source, (↑toOpenPartialHomeomorph_1 p).1 = proj p},
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun } =
      { toOpenPartialHomeomorph := toOpenPartialHomeomorph_1, baseSet := baseSet_1, open_baseSet := open_baseSet_1,
        source_eq := source_eq_1, target_eq := target_eq_1, proj_toFun := proj_toFun_1 } →
    toOpenPartialHomeomorph = toOpenPartialHomeomorph_1 ∧ baseSet = baseSet_1
-- Init.Grind.Ring.Basic
_private.Init.Grind.Ring.Basic.0.Lean.Grind.Ring.intCast_mul_aux : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (x y : ℕ), ↑(↑x * ↑y) = ↑x * ↑y
-- Mathlib.RingTheory.FinitePresentation
/-- The ring of polynomials in finitely many variables is finitely presented.  -/
_private.Mathlib.RingTheory.FinitePresentation.0.Algebra.FinitePresentation.mvPolynomial_aux : ∀ (R : Type w₁) [inst : CommRing R] (ι : Type u_1) [Finite ι], Algebra.FinitePresentation R (MvPolynomial ι R)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_baseChange : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {A : Type u_7} {B : Type u_8}
  [inst_5 : CommSemiring A] [inst_6 : Algebra R A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Algebra A B]
  [inst_10 : IsScalarTower R A B] (f : M →ₗ[R] N),
  LinearMap.baseChange B (LinearMap.baseChange A f) =
    ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B N).symm ∘ₗ
      LinearMap.baseChange B f ∘ₗ ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B M)
-- Mathlib.Algebra.Group.ForwardDiff
/-- Forward difference operator, `fwdDiff h f n = f (n + h) - f n`. The notation `Δ_[h]` for this
operator is available in the `fwdDiff` namespace.
 -/
fwdDiff : {M : Type u_1} → {G : Type u_2} → [AddCommMonoid M] → [AddCommGroup G] → M → (M → G) → M → G
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {V : ↑X.affineOpens} (f : ↑(X.presheaf.obj (Opposite.op ↑V))),
  AlgebraicGeometry.Scheme.Hom.opensRange (I.glueDataObjMap ⋯) =
    (TopologicalSpace.Opens.map (I.glueDataObjι V).base).obj
      ((TopologicalSpace.Opens.map (↑V).ι.base).obj (X.basicOpen f))
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- The [Kurosh problem](https://en.wikipedia.org/wiki/Kurosh_problem) asks to show that
  this is still true when `A` is not necessarily commutative and `R` is a field, but it has
  been solved in the negative. See https://arxiv.org/pdf/1706.02383.pdf for criteria for a
  finitely generated algebraic (= integral) algebra over a field to be finite dimensional.

This could be an `instance`, but we tend to go from `Module.Finite` to `IsIntegral`/`IsAlgebraic`,
and making it an instance will cause the search to be complicated a lot.
 -/
Algebra.IsIntegral.finite : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] [h' : Algebra.FiniteType R A], Module.Finite R A
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
EReal.tendsto_exp_nhds_bot_nhds_zero : Filter.Tendsto EReal.exp (nhds ⊥) (nhds 0)
-- Mathlib.Analysis.InnerProductSpace.PiL2
FiniteDimensional.toBasis_orthonormalBasisSingleton : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : Unique ι] (h : Module.finrank 𝕜 E = 1) {v : E}
  (hv : ‖v‖ = 1),
  (FiniteDimensional.orthonormalBasisSingleton ι 𝕜 h v hv).toBasis = FiniteDimensional.basisSingleton ι h v ⋯
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.shift_distinguished_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C) (n : ℤ),
  (CategoryTheory.shiftFunctor (CategoryTheory.Pretriangulated.Triangle C) n).obj T ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles ↔
    T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.GroupTheory.Coset.Basic
/-- An equivalence between any two non-empty fibers of an `AddMonoidHom`.  -/
AddMonoidHom.fiberEquiv : {α : Type u_1} →
  [inst : AddGroup α] →
    {H : Type u_2} → [inst_1 : AddGroup H] → (f : α →+ H) → (a b : α) → ↑(⇑f ⁻¹' {f a}) ≃ ↑(⇑f ⁻¹' {f b})
-- Mathlib.Data.Finset.Insert
Finset.eq_empty_of_ssubset_singleton : ∀ {α : Type u_1} {s : Finset α} {x : α}, s ⊂ {x} → s = ∅
-- Mathlib.Data.Ordmap.Ordnode
/-- **Internal use only**, because it requires a balancing constraint on the inputs.

O(log n). Extract and remove the minimum element from a nonempty tree.  -/
Ordnode.splitMin' : {α : Type u_1} → Ordnode α → α → Ordnode α → α × Ordnode α
-- Mathlib.Topology.EMetricSpace.Defs
Metric.closedEBall_prod_same : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal),
  Metric.closedEBall x r ×ˢ Metric.closedEBall y r = Metric.closedEBall (x, y) r
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeriesBilinear_radius : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F),
  (f.fpowerSeriesBilinear x).radius = ⊤
-- Mathlib.Data.Set.Sups
Set.sups_union_left : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s₁ s₂ t : Set α}, (s₁ ∪ s₂) ⊻ t = s₁ ⊻ t ∪ s₂ ⊻ t
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.initiallySmall_of_essentiallySmall_weakly_initial_objectProperty : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.IsCofilteredOrEmpty J]
  (P : CategoryTheory.ObjectProperty J) [CategoryTheory.ObjectProperty.EssentiallySmall.{v, v, u} P],
  (∀ (i : J), ∃ j, P j ∧ Nonempty (j ⟶ i)) → CategoryTheory.InitiallySmall J
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.IsSubordinate.toPartitionOfUnity : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} {f : BumpCovering ι X s} {U : ι → Set X},
  f.IsSubordinate U → f.toPartitionOfUnity.IsSubordinate U
-- Mathlib.Data.Stream.Defs
/-- Tails of a stream, starting with `Stream'.tail s`.  -/
Stream'.tails : {α : Type u} → Stream' α → Stream' (Stream' α)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If a measurable space has a finite measure `μ` and a countable additive group `G` acts
quasi-measure-preservingly, then to show that a set `s` is a fundamental domain, it is sufficient
to check that its translates `g +ᵥ s` are (almost) disjoint and that the sum `∑' g, μ (g +ᵥ s)` is
sufficiently large.  -/
MeasureTheory.IsAddFundamentalDomain.mk_of_measure_univ_le : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [Countable G],
  MeasureTheory.NullMeasurableSet s μ →
    (∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s) →
      (∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g +ᵥ x) μ μ) →
        μ Set.univ ≤ ∑' (g : G), μ (g +ᵥ s) → MeasureTheory.IsAddFundamentalDomain G s μ
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_lt_left_iff_lt : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : PartialOrder k] [IsOrderedRing k] [inst_3 : AddCommGroup E]
  [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k}
  [PosSMulReflectLT k E], 0 < r → ((AffineMap.lineMap a b) r < a ↔ b < a)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A binary fan with vertex `P` consists of the two projections `π₁ : P ⟶ X` and `π₂ : P ⟶ Y`.  -/
CategoryTheory.Limits.BinaryFan.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y P : C} → (P ⟶ X) → (P ⟶ Y) → CategoryTheory.Limits.BinaryFan X Y
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂},
  (m₁ ∪ m₂).get k h' = m₂.get k ⋯
-- Mathlib.Data.List.Cycle
List.next.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] (l l_1 : List α) (e_l : l = l_1) (x x_1 : α) (e_x : x = x_1) (h : x ∈ l),
  l.next x h = l_1.next x_1 ⋯
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.ofSubmodule'_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M₂] [inst_5 : TopologicalSpace M₂]
  {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M ≃SL[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : ↥U),
  ↑((f.ofSubmodule' U).symm x) = f.symm ↑x
-- Mathlib.Logic.Lemmas
ite_ite_distrib_right : ∀ {α : Sort u_1} {p q : Prop} [inst : Decidable p] [inst_1 : Decidable q] {a b c : α},
  (if p then if q then a else b else c) = if q then if p then a else c else if p then b else c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.toCommSq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P}, CategoryTheory.IsPushout f g inl inr → CategoryTheory.CommSq f g inl inr
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Replacing both the first and third points by ones on the same lines but the opposite rays
does not change the oriented angle (vertically opposite angles).  -/
Sbtw.oangle_eq_left_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₁' p₂ p₃ p₃' : P},
  Sbtw ℝ p₁ p₂ p₁' → Sbtw ℝ p₃ p₂ p₃' → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃'
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.frobeniusRotationCoeff.congr_simp : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  {a₁ a₁_1 : WittVector p k} (e_a₁ : a₁ = a₁_1) {a₂ a₂_1 : WittVector p k} (e_a₂ : a₂ = a₂_1) (ha₁ : a₁.coeff 0 ≠ 0)
  (ha₂ : a₂.coeff 0 ≠ 0) (a a_1 : ℕ),
  a = a_1 → WittVector.frobeniusRotationCoeff p ha₁ ha₂ a = WittVector.frobeniusRotationCoeff p ⋯ ⋯ a_1
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.iSup_adj : ∀ {ι : Sort u_1} {V : Type u} {a b : V} {f : ι → SimpleGraph V}, (⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.PlausibleStep.yieldSome : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α}
  {f : β → Std.Iterators.PostconditionT n (Option γ)} [inst : Std.Iterator α m β] {it : Std.IterM n γ}
  {it' : Std.IterM m β} {out : β} {out' : γ},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out) →
    (f out).Property (some out') →
      Std.Iterators.Types.FilterMap.PlausibleStep it
        (Std.IterStep.yield (Std.IterM.InternalCombinators.filterMap lift f it') out')
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ico_zpow : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ico (b ^ n) (b ^ (n + 1)))
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.intersperseTR.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x y : α) (xs : List α) (h_1 : Unit → motive [])
  (h_2 : (x : α) → motive [x]) (h_3 : (x y : α) → (xs : List α) → motive (x :: y :: xs)),
  (match x :: y :: xs with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: y :: xs => h_3 x y xs) =
    h_3 x y xs
-- Mathlib.Combinatorics.Quiver.Path.Vertices
/-- Given a path `p : Path a b` and an index `n ≤ p.length`,
we can split `p = p₁.comp p₂` with `p₁.length = n`.  -/
Quiver.Path.exists_eq_comp_of_le_length : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) {n : ℕ},
  n ≤ p.length → ∃ v p₁ p₂, p = p₁.comp p₂ ∧ p₁.length = n
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_comm : ∀ {γ : Type w} {ι₁ : Type u_3} {ι₂ : Type u_4} {β₁ : ι₁ → Type u_1} {β₂ : ι₂ → Type u_2} [inst : DecidableEq ι₁]
  [inst_1 : DecidableEq ι₂] [inst_2 : (i : ι₁) → Zero (β₁ i)] [inst_3 : (i : ι₂) → Zero (β₂ i)]
  [inst_4 : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)] [inst_5 : (i : ι₂) → (x : β₂ i) → Decidable (x ≠ 0)]
  [inst_6 : CommMonoid γ] (f₁ : Π₀ (i : ι₁), β₁ i) (f₂ : Π₀ (i : ι₂), β₂ i) (h : (i : ι₁) → β₁ i → (i : ι₂) → β₂ i → γ),
  (f₁.prod fun i₁ x₁ => f₂.prod fun i₂ x₂ => h i₁ x₁ i₂ x₂) = f₂.prod fun i₂ x₂ => f₁.prod fun i₁ x₁ => h i₁ x₁ i₂ x₂
-- Init.Data.List.Attach
List.attach_congr : ∀ {α : Type u_1} {l₁ l₂ : List α} (h : l₁ = l₂), l₁.attach = List.map (fun x => ⟨↑x, ⋯⟩) l₂.attach
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_pos_of_pos_of_lt_pi : ∀ {x : ℝ}, 0 < x → x < Real.pi → 0 < Real.sin x
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mk.inj : ∀ {α : Type u_2} {inst : TopologicalSpace α} {carrier : Set α} {is_open' : IsOpen carrier} {carrier_1 : Set α}
  {is_open'_1 : IsOpen carrier_1},
  { carrier := carrier, is_open' := is_open' } = { carrier := carrier_1, is_open' := is_open'_1 } → carrier = carrier_1
-- Mathlib.Analysis.Normed.Algebra.Spectrum
Real.spectralRadius_mem_spectrum : ∀ {A : Type u_4} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] {a : A},
  (spectrum ℝ a).Nonempty → SpectrumRestricts a ⇑ContinuousMap.realToNNReal → (spectralRadius ℝ a).toReal ∈ spectrum ℝ a
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.instInhabitedScore : Inhabited Lean.FuzzyMatching.Score✝
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNatCastQuotient : {R : Type u_1} → [inst : AddMonoidWithOne R] → [inst_1 : Mul R] → (c : RingCon R) → NatCast c.Quotient
-- Init.WF
WellFounded.induction : ∀ {α : Sort u} {r : α → α → Prop},
  WellFounded r → ∀ {C : α → Prop} (a : α), (∀ (x : α), (∀ (y : α), r y x → C y) → C x) → C a
-- Init.Control.State
/-- Executes an action from a monad with added state in the underlying monad `m`. Given an initial
state, it returns a value paired with the final state.
 -/
StateT.run : {σ : Type u} → {m : Type u → Type v} → {α : Type u} → StateT σ m α → σ → m (α × σ)
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `finsum_pos`. -/
finsum_pos' : ∀ {ι : Type u_3} {M : Type u_7} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M]
  {f : ι → M}, (∀ (i : ι), 0 ≤ f i) → (∃ i, 0 < f i) → Function.HasFiniteSupport f → 0 < ∑ᶠ (i : ι), f i
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_inj : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : Zero α] [inst_1 : DecidableEq o]
  {M N : o → Matrix m n α}, Matrix.blockDiagonal M = Matrix.blockDiagonal N ↔ M = N
-- Mathlib.Algebra.Group.TransferInstance
Equiv.addEquiv.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Add β], e.addEquiv = { toEquiv := e, map_add' := ⋯ }
-- Mathlib.Order.Minimal
minimal_true_subtype : ∀ {α : Type u_2} {P : α → Prop} [inst : LE α] {x : Subtype P}, Minimal (fun x => True) x ↔ Minimal P ↑x
-- Mathlib.Logic.Embedding.Set
subtypeOrEquiv_symm_inl : ∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] (h : Disjoint p q) (x : { x // p x }),
  (subtypeOrEquiv p q h).symm (Sum.inl x) = ⟨↑x, ⋯⟩
-- Std.Data.HashSet.Lemmas
Std.HashSet.insertMany_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {l : List α} {k : α},
  m.insertMany (k :: l) = (m.insert k).insertMany l
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.WPath.root.injEq : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} (a : P.A) (f : P.last.B a → P.last.W) (i : Fin2 n) (c c_1 : P.drop.B a i),
  (MvPFunctor.WPath.root a f i c = MvPFunctor.WPath.root a f i c_1) = (c = c_1)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- An integral domain in which there is an irreducible element `p`
such that every nonzero element is associated to a power of `p`
is a discrete valuation ring.
 -/
IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R],
  IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R → IsDiscreteValuationRing R
-- Mathlib.Topology.LocallyFinsupp
/-- Taking the negative part of a function with locally finite support commutes with
scalar multiplication by a natural number.
 -/
Function.locallyFinsuppWithin.nsmul_negPart : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommGroup Y]
  [inst_2 : LinearOrder Y] [IsOrderedAddMonoid Y] (n : ℕ) (f : Function.locallyFinsuppWithin U Y), (n • f)⁻ = n • f⁻
-- Lean.Meta.Basic
Lean.Meta.ParamInfo.isImplicit : Lean.Meta.ParamInfo → Bool
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Icc_atBot_atBot : ∀ {α : Type u_1} [inst : Preorder α], Filter.TendstoIxxClass Set.Icc Filter.atBot Filter.atBot
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.surjective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), Function.Surjective ⇑e
-- Batteries.Data.List.Lemmas
List.idxOfNth_cons_succ : ∀ {α : Type u_1} {xs : List α} {x : α} {n : ℕ} [inst : BEq α] {a : α},
  List.idxOfNth x (a :: xs) (n + 1) =
    if (a == x) = true then List.idxOfNth x xs n + 1 else List.idxOfNth x xs (n + 1) + 1
-- Mathlib.Topology.List
nhds_cons : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (l : List α), nhds (a :: l) = List.cons <$> nhds a <*> nhds l
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
Filter.EventuallyEq.mlieBracketWithin_vectorField_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M}
  {V W V₁ W₁ : (x : M) → TangentSpace I x},
  V₁ =ᶠ[nhdsWithin x s] V →
    V₁ x = V x →
      W₁ =ᶠ[nhdsWithin x s] W →
        W₁ x = W x → VectorField.mlieBracketWithin I V₁ W₁ s x = VectorField.mlieBracketWithin I V W s x
-- Mathlib.FieldTheory.Fixed
FixedPoints.smulCommClass' : ∀ (M : Type u) [inst : Monoid M] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction M F],
  SMulCommClass (↥(FixedPoints.subfield M F)) M F
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformly.hasSum : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {x : β}
  [inst_1 : UniformSpace α], HasSumUniformly f g → HasSum (fun x_1 => f x_1 x) (g x)
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.mk : {R : Type u_1} → [inst : CommRing R] → (toSubring : Subring R) → [isLocalRing : IsLocalRing ↥toSubring] → LocalSubring R
-- Mathlib.Computability.EpsilonNFA
εNFA.mk.injEq : ∀ {α : Type u} {σ : Type v} (step : σ → Option α → Set σ) (start accept : Set σ) (step_1 : σ → Option α → Set σ)
  (start_1 accept_1 : Set σ),
  ({ step := step, start := start, accept := accept } = { step := step_1, start := start_1, accept := accept_1 }) =
    (step = step_1 ∧ start = start_1 ∧ accept = accept_1)
-- Mathlib.Data.FunLike.IsApply
IsAddApply.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [inst : FunLike F α β] [inst_1 : Add β]
  [inst_2 : Add F], (∀ (f g : F) (x : α), (f + g) x = f x + g x) → IsAddApply F α β
-- Mathlib.Control.Functor
Functor.instInhabitedAddConst : {α : Type u_1} → {β : Type u_2} → [Inhabited α] → Inhabited (Functor.AddConst α β)
-- Init.Data.Dyadic.Basic
Int.two_pow_trailingZeros_dvd : ∀ {i : ℤ}, i ≠ 0 → 2 ^ i.trailingZeros ∣ i
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel_arrow_assoc : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [inst_3 : CategoryTheory.Limits.HasKernel g]
  (w : CategoryTheory.CategoryStruct.comp f g = 0) {Z : V} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (imageToKernel f g w)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject g).arrow h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h
-- Init.Data.Array.Count
Array.countP.eq_1 : ∀ {α : Type u} (p : α → Bool) (as : Array α),
  Array.countP p as = Array.foldr (fun a acc => bif p a then acc + 1 else acc) 0 as
-- Mathlib.Analysis.Normed.Group.Pointwise
smul_ball_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), x • Metric.ball 1 δ = Metric.ball x δ
-- Mathlib.Analysis.Analytic.Basic
AnalyticWithinAt.continuousWithinAt_insert : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E},
  AnalyticWithinAt 𝕜 f s x → ContinuousWithinAt f (insert x s) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_union! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁.union! m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.whiskerRight_left_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T) {Z : C} (h : T.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst T.hom R.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.hom R.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f) h)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap_ι_assoc : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens) (h : U ≤ V)
  {Z : AlgebraicGeometry.Scheme} (h_1 : I.glueData.glued ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.glueDataObjMap h) (CategoryTheory.CategoryStruct.comp (I.glueData.ι V) h_1) =
    CategoryTheory.CategoryStruct.comp (I.glueData.ι U) h_1