mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.LogConfig.mk.inj : ∀ {logDir? : Option System.FilePath} {allowedMethods? disallowedMethods? : Option (Std.HashSet String)}
  {logDir?_1 : Option System.FilePath} {allowedMethods?_1 disallowedMethods?_1 : Option (Std.HashSet String)},
  { logDir? := logDir?, allowedMethods? := allowedMethods?, disallowedMethods? := disallowedMethods? } =
      { logDir? := logDir?_1, allowedMethods? := allowedMethods?_1, disallowedMethods? := disallowedMethods?_1 } →
    logDir? = logDir?_1 ∧ allowedMethods? = allowedMethods?_1 ∧ disallowedMethods? = disallowedMethods?_1
-- Init.System.Promise
_private.Init.System.Promise.0.IO.Promise.h : ∀ {α : Type} (self : IO.Promise α), Nonempty α
-- Init.Data.UInt.Bitwise
UInt64.ofNat_and : ∀ (a b : ℕ), UInt64.ofNat (a &&& b) = UInt64.ofNat a &&& UInt64.ofNat b
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_smul_iff_of_neg_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β] [PosSMulReflectLT α β], a < 0 → (a • b₁ < a • b₂ ↔ b₂ < b₁)
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.encard_neg : ∀ {G : Type u_1} [inst : InvolutiveNeg G] (s : Set G), (-s).encard = s.encard
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.instInhabited : {R : Type uR} →
  {A₁ : Type uA₁} → [inst : CommSemiring R] → [inst_1 : Semiring A₁] → [inst_2 : Algebra R A₁] → Inhabited (A₁ ≃ₐ[R] A₁)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β k} {fallback : α}, (cmp (t.maxKeyD fallback) ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.closure_union : ∀ {M : Type u_1} [inst : Add M] (s t : Set M),
  AddSubsemigroup.closure (s ∪ t) = AddSubsemigroup.closure s ⊔ AddSubsemigroup.closure t
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Function.Surjective ⇑(Monoid.Coprod.swap M N)
-- Mathlib.Data.Fin.Tuple.Sort
/-- If two permutations of a tuple `f` are both antitone, then they are equal.  -/
Tuple.unique_antitone : ∀ {n : ℕ} {α : Type u_1} [inst : PartialOrder α] {f : Fin n → α} {σ τ : Equiv.Perm (Fin n)},
  Antitone (f ∘ ⇑σ) → Antitone (f ∘ ⇑τ) → f ∘ ⇑σ = f ∘ ⇑τ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instHashableExpr.hash : Lean.Grind.CommRing.Expr → UInt64
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Quiver.FreeGroupoid.congr_reverse : ∀ {V : Type u} [inst : Quiver V] {X Y : CategoryTheory.Paths (Quiver.Symmetrify V)} (p q : X ⟶ Y),
  CategoryTheory.HomRel.CompClosure Quiver.FreeGroupoid.redStep p q →
    CategoryTheory.HomRel.CompClosure Quiver.FreeGroupoid.redStep (Quiver.Path.reverse p) (Quiver.Path.reverse q)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.negDvdTight.injEq : ∀ (c₁ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) (c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr)
  (c₁_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) (c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.negDvdTight c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.negDvdTight c₁_1 c₂_1) =
    (c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.add_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {T : C}
  (f : T ⟶ S), (E.add f).I₀ = Option E.I₀
-- Mathlib.Topology.Algebra.Monoid
/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `l` be a filter on `M` which is disjoint from the cocompact filter. Then, the multiplication map
`M × M → M` tends to zero on the filter product `l ×ˢ 𝓝 0`.  -/
tendsto_mul_prod_nhds_zero_of_disjoint_cocompact : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : MulZeroClass M] [ContinuousMul M] {l : Filter M},
  Disjoint l (Filter.cocompact M) → Filter.Tendsto (fun x => x.1 * x.2) (l ×ˢ nhds 0) (nhds 0)
-- Mathlib.Algebra.Notation.Support
Function.notMem_support : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M} {x : ι}, x ∉ Function.support f ↔ f x = 0
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp_supports : ∀ {S : Finset Turing.PartrecToTM2.Λ'} {c : Turing.ToPartrec.Code} {k : Turing.PartrecToTM2.Cont'},
  Turing.PartrecToTM2.codeSupp c k ⊆ S → Turing.PartrecToTM2.Supports (Turing.PartrecToTM2.codeSupp c k) S
-- Mathlib.Order.Sublattice
Sublattice.mem_sInf : ∀ {α : Type u_2} [inst : Lattice α] {a : α} {S : Set (Sublattice α)}, a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instOrderTop : {α : Type u_1} → [inst : Preorder α] → [BoundedOrder α] → OrderTop (NonemptyInterval α)
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
Finsupp.toFreeAbelianGroup_comp_toFinsupp : ∀ {X : Type u_1}, Finsupp.toFreeAbelianGroup.comp FreeAbelianGroup.toFinsupp = AddMonoidHom.id (FreeAbelianGroup X)
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_mul : ∀ (a b : UInt64), (a * b).toUInt32 = a.toUInt32 * b.toUInt32
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiff.sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n fun x => ∑ i ∈ t, f i x
-- Mathlib.Util.Qq
/-- Returns a proof of `p : Prop` using `decide p`.

This is a Qq version of `Lean.Meta.mkDecideProof`.  -/
Qq.mkDecideProofQ : (p : Q(Prop)) → Lean.MetaM Q(«$p»)
-- Init.Data.Iterators.Lemmas.Monadic.Basic
/-- Induction principle for finite monadic iterators: One can define a function `f` that maps every
iterator `it` to an element of `motive it` by defining `f it` in terms of the values of `f` on
the plausible successors of `it'.
 -/
Std.IterM.inductSteps : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        [Std.Iterators.Finite α m] →
          (motive : Std.IterM m β → Sort x) →
            ((it : Std.IterM m β) →
                ({it' : Std.IterM m β} → {out : β} → it.IsPlausibleStep (Std.IterStep.yield it' out) → motive it') →
                  ({it' : Std.IterM m β} → it.IsPlausibleStep (Std.IterStep.skip it') → motive it') → motive it) →
              (it : Std.IterM m β) → motive it
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ_ofNat : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℕ),
  W.Ψ ↑n = Polynomial.C (W.preΨ' n) * if Even n then W.ψ₂ else 1
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- `n + 2` points are affinely independent if and only if their
`vectorSpan` does not have dimension at most `n`.  -/
affineIndependent_iff_not_finrank_vectorSpan_le : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] (p : ι → P) {n : ℕ},
  Fintype.card ι = n + 2 → (AffineIndependent k p ↔ ¬Module.finrank k ↥(vectorSpan k (Set.range p)) ≤ n)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.associator_hom_apply : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {X Y Z : (i : I) → C i} {i : I},
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom i =
    (CategoryTheory.MonoidalCategoryStruct.associator (X i) (Y i) (Z i)).hom
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the reverse direction of `mdifferentiableOn_iff_differentiableOn`.

---

For maps between vector spaces, `MDifferentiableOn` and `DifferentiableOn` coincide  -/
DifferentiableOn.mdifferentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {s : Set E}, DifferentiableOn 𝕜 f s → MDiff[s] f
-- Mathlib.Algebra.Lie.Weights.Basic
/-- See also `LieModule.iSup_ucs_eq_genWeightSpace_zero`.  -/
LieModule.iInf_lowerCentralSeries_eq_posFittingComp : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsNoetherian R M] [IsArtinian R M],
  ⨅ k, LieModule.lowerCentralSeries R L M k = LieModule.posFittingComp R L M
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.universalAddHom_commutes : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {T : Type u_2}
  [inst_2 : AddMonoid T] (f : R →+ T) (fS : ↥S →+ AddUnits T) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) {r : R},
  (AddOreLocalization.universalAddHom f fS hf) (AddOreLocalization.numeratorHom r) = f r
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- An alternative formulation of `mdifferentiableWithinAt_iff_of_mem_maximalAtlas`
if the set if `s` lies in `e.source`.  -/
mdifferentiableWithinAt_iff_image : ∀ {𝕜 : 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'} {s : Set M}
  {e : OpenPartialHomeomorph M H} {e' : OpenPartialHomeomorph M' H'} {x : M},
  e ∈ IsManifold.maximalAtlas I 1 M →
    e' ∈ IsManifold.maximalAtlas I' 1 M' →
      s ⊆ e.source →
        x ∈ e.source →
          f x ∈ e'.source →
            (MDiffAt[s] f x ↔
              ContinuousWithinAt f s x ∧
                DifferentiableWithinAt 𝕜 (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)
                  (↑(e.extend I) x))
-- Init.Data.Int.DivMod.Basic
/-- The `Div Int` and `Mod Int` instances use `Int.ediv` and `Int.emod` for compatibility with SMT-LIB and
because mathematical reasoning tends to be easier.
 -/
Int.instMod : Mod ℤ
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.ringEquivFixedPoints_apply_coe : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_4) [inst : Group G] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B] [hA : IsGaloisGroup G A B] [inst_5 : FaithfulSMul A B]
  (x : A), ↑((IsGaloisGroup.ringEquivFixedPoints G A B) x) = (algebraMap A B) x
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.CommShift₂Setup.z_zero₁ : ∀ {D : Type u_5} [inst : CategoryTheory.Category.{v_5, u_5} D] {M : Type u_6} [inst_1 : AddCommMonoid M]
  [inst_2 : CategoryTheory.HasShift D M] (self : CategoryTheory.CommShift₂Setup D M) (m₁ m₂ : M),
  self.z (0, m₁) (0, m₂) = 1
-- Std.Sync.CancellationContext
/-- Returns the cancellation reason if the context is cancelled.
 -/
Std.CancellationContext.getCancellationReason : Std.CancellationContext → BaseIO (Option Std.CancellationReason)
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.eq_left : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ t₃ t₄ : String}, p.Splits t₁ t₂ → p.Splits t₃ t₄ → t₁ = t₃
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.Prod.invFun'.eq_1 : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)] (p : B × F₁ × F₂),
  Bundle.Trivialization.Prod.invFun' e₁ e₂ p = ⟨p.1, (e₁.symm p.1 p.2.1, e₂.symm p.1 p.2.2)⟩
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₂₃Functor_obj_obj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (G : C₁) (k : C₃) {X Y : C₂}
  (f : X ⟶ Y), (((CategoryTheory.Functor.flip₂₃Functor.obj F).obj G).obj k).map f = ((F.obj G).map f).app k
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory)
      (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C)))
  (X_1 : SimplexCategory),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.counitIso.inv.app X).right.app X_1 =
    CategoryTheory.CategoryStruct.id
      (match CategoryTheory.WithInitial.incl.obj X_1 with
      | CategoryTheory.WithInitial.of x => X.right.obj x
      | CategoryTheory.WithInitial.star => X.left)
-- Mathlib.Data.Finset.Card
Finset.card_le_one_iff_subset_singleton : ∀ {α : Type u_1} {s : Finset α} [Nonempty α], s.card ≤ 1 ↔ ∃ x, s ⊆ {x}
-- Init.Data.Array.Range
Array.mem_range'_1 : ∀ {s n m : ℕ}, m ∈ Array.range' s n ↔ s ≤ m ∧ m < s + n
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_eq_zero : ∀ {q : ℚ}, q.toNNRat = 0 ↔ q ≤ 0
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instForInValuesOfMonad : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → {m : Type u_1 → Type u_2} → [Monad m] → ForIn m (RBTree.RBMap.Values α β cmp) β
-- Init.Data.Range.Polymorphic.UInt
UInt32.rxcHasSize_eq_toBitVec : ∀ {lo : BitVec 32} {hi : UInt32}, Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofHasPushout_inr : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂)
  [inst_3 : CategoryTheory.Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)],
  (CategoryTheory.Functor.PushoutObjObj.ofHasPushout F f₁ f₂).inr =
    CategoryTheory.Limits.pushout.inr ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
-- Lean.Elab.Deriving.Basic
_private.Lean.Elab.Deriving.Basic.0.Lean.Elab.Term.MkInstResult.mk.inj : ∀ {instType instVal instType_1 instVal_1 : Lean.Expr},
  { instType := instType, instVal := instVal } = { instType := instType_1, instVal := instVal_1 } →
    instType = instType_1 ∧ instVal = instVal_1
-- Mathlib.GroupTheory.GroupAction.Hom
/-- If `DistribMulAction` of `M` and `N` on `A` commute,
then for each `c : M`, `(c • ·)` is an `N`-action additive homomorphism.  -/
SMulCommClass.toDistribMulActionHom : {M : Type u_13} →
  (N : Type u_11) →
    (A : Type u_12) →
      [inst : Monoid N] →
        [inst_1 : AddMonoid A] →
          [inst_2 : DistribSMul M A] → [inst_3 : DistribMulAction N A] → [SMulCommClass M N A] → M → A →+[N] A
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LocalPresentationAt.mem_domChart_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop}
  (self : Manifold.LocalPresentationAt I J n f x P), x ∈ self.domChart.source
-- Mathlib.Algebra.MvPolynomial.NoZeroDivisors
MvPolynomial.degrees_mul_eq : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] {p q : MvPolynomial σ R} [NoZeroDivisors R],
  p ≠ 0 → q ≠ 0 → (p * q).degrees = p.degrees + q.degrees
-- Mathlib.Algebra.Group.Embedding
addRightEmbedding_apply : ∀ {G : Type u_1} [inst : Add G] [inst_1 : IsRightCancelAdd G] (g h : G), (addRightEmbedding g) h = h + g
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply_ker : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E}
  (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented) (y : ↥(↑f').ker),
  ↑(HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker) (↑y + a) = (f (↑y + a), y)
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- The recurrence relation satisfied by the Fibonacci sequence.  -/
Real.fibRec : {α : Type u_1} → [inst : CommSemiring α] → LinearRecurrence α
-- Lean.MetavarContext
Lean.MetavarContext.revert : Array Lean.Expr → Lean.MVarId → Bool → Lean.MetavarContext.MkBindingM (Lean.Expr × Array Lean.Expr)
-- Init.Data.SInt.Bitwise
Int16.ofBitVec_or : ∀ (a b : BitVec 16), Int16.ofBitVec (a ||| b) = Int16.ofBitVec a ||| Int16.ofBitVec b
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.getKey? t.maxKey! = some t.maxKey!
-- Init.Data.Fin.Lemmas
/-- Proves a statement by induction on the underlying `Nat` value in a `Fin (n + 1)`.

For the induction:
 * `zero` is the base case, demonstrating `motive 0`.
 * `succ` is the inductive step, assuming the motive for `i : Fin n` (lifted to `Fin (n + 1)` with
   `Fin.castSucc`) and demonstrating it for `i.succ`.

`Fin.inductionOn` is a version of this induction principle that takes the `Fin` as its first
parameter, `Fin.cases` is the corresponding case analysis operator, and `Fin.reverseInduction` is a
version that starts at the greatest value instead of `0`.
 -/
Fin.induction : {n : ℕ} →
  {motive : Fin (n + 1) → Sort u_1} →
    motive 0 → ((i : Fin n) → motive i.castSucc → motive i.succ) → (i : Fin (n + 1)) → motive i
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.all : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.BoundedFormula α (n + 1)},
  T.Iff φ ψ → T.Iff φ.all ψ.all
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  {f : (a : α) → β a → Bool} {k : α} (h : t.WF)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filter! f t) = true},
  (Std.DTreeMap.Internal.Impl.filter! f t).getKey k h' = t.getKey k ⋯
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.fold_eq_foldl_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {δ : Type w} {β : Type v} {m : Std.DHashMap α fun x => β}
  {f : δ → α → β → δ} {init : δ},
  Std.DHashMap.fold f init m = Array.foldl (fun a b => f a b.1 b.2) init (Std.DHashMap.Const.toArray m)
-- Mathlib.Combinatorics.Graph.Basic
/-- `Graph.copy` produces a graph equal to `G` but with provided definitional choices
for `vertexSet`, `edgeSet`, and `IsLink`. This is mainly useful for improving
definitional equalities while keeping the same underlying graph.  -/
Graph.copy : {α : Type u_1} →
  {β : Type u_2} →
    (G : Graph α β) →
      {vertexSet : Set α} →
        {edgeSet : Set β} →
          {IsLink : β → α → α → Prop} →
            G.vertexSet = vertexSet →
              G.edgeSet = edgeSet → (∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y) → Graph α β
-- Mathlib.Data.Nat.Choose.Basic
/-- Show that `Nat.choose` is increasing for small values of the right argument.  -/
Nat.choose_le_succ_of_lt_half_left : ∀ {r n : ℕ}, r < n / 2 → n.choose r ≤ n.choose (r + 1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α},
  (Std.DTreeMap.filter f t).getKey? k = (t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.himp_def : ∀ {α : Type u_1} {s t : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α], s ⇨ t = t ∪ sᶜ
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.inv_mem_units_iff : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) {x : Mˣ}, x⁻¹ ∈ S.units ↔ x ∈ S.units
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.inv_toEquiv : ∀ (G : Type u_4) [inst : MeasurableSpace G] [inst_1 : InvolutiveInv G] [inst_2 : MeasurableInv G],
  (MeasurableEquiv.inv G).toEquiv = Equiv.inv G
-- Mathlib.Order.Bounds.Basic
isLUB_singleton : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsLUB {a} a
-- Init.Internal.Order.MonadTail
StateT.bind.eq_1 : ∀ {σ : Type u} {m : Type u → Type v} [inst : Monad m] {α β : Type u} (x : StateT σ m α) (f : α → StateT σ m β) (s : σ),
  x.bind f s = do
    let __x ← x s
    match __x with
      | (a, s) => f a s
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.norm.eq_1 : ∀ (k : ℤ), (Int.Internal.Linear.Poly.num k).norm = Int.Internal.Linear.Poly.num k
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.freeYonedaEquiv_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M N : PresheafOfModules R} {X : C} (m : (PresheafOfModules.free R).obj (CategoryTheory.yoneda.obj X) ⟶ M)
  (φ : M ⟶ N),
  PresheafOfModules.freeYonedaEquiv (CategoryTheory.CategoryStruct.comp m φ) =
    (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op X))) (PresheafOfModules.freeYonedaEquiv m)
-- Mathlib.Order.PiLex
/-- `Lex (∀ i, α i)` is a linear order if the original order has well-founded `<`.  -/
Pi.Lex.linearOrder : {ι : Type u_1} →
  {β : ι → Type u_2} →
    [inst : LinearOrder ι] → [WellFoundedLT ι] → [(a : ι) → LinearOrder (β a)] → LinearOrder (Lex ((i : ι) → β i))
-- Mathlib.Order.Filter.Basic
Filter.set_eventuallyLE_iff_mem_inf_principal : ∀ {α : Type u} {s t : Set α} {l : Filter α}, s ≤ᶠ[l] t ↔ t ∈ l ⊓ Filter.principal s
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryGT! : {α : Type u} → {β : Type v} → [Ord α] → [Inhabited (α × β)] → α → (Std.DTreeMap.Internal.Impl α fun x => β) → α × β
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.forget₂Mon_map_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommMon C} (f : A ⟶ B),
  ((CategoryTheory.CommMon.forget₂Mon C).map f).hom = f.hom.hom