mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.pullback.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : AddGroup A] [inst_1 : AddGroup B]
  [inst_2 : AddGroup C] [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C]
  {φ : A →+ B} {ψ : B →+ C} (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A]
  [inst_7 : IsTopologicalAddGroup B] [inst_8 : NormedAddCommGroup E] (f : CompactlySupportedContinuousMap B E) (b : B),
  H.pullback f b = CompactlySupportedContinuousMap.pullback_addMonoidHom ⋯ f b
-- Mathlib.Data.Set.Basic
Set.le_eq_subset : ∀ {α : Type u}, (fun x1 x2 => x1 ⊆ x2) = fun x1 x2 => x1 ⊆ x2
-- Init.Meta.Defs
Lean.HygieneInfo.mkIdent : Lean.HygieneInfo → Lean.Name → optParam Bool false → Lean.Ident
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.natDegree_divX_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.divX.natDegree ≤ p.natDegree
-- Init.Data.String.Basic
String.Pos.Raw.utf8PrevAux : List Char → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_desc_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
  (hc : ∀ (j : ι), ∃ i, c.Rel i j) (i j : ι),
  CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).hom i j)
      ((HomologicalComplex.homotopyCofiber.desc φ α hα).f j) =
    hα.hom i j
-- Mathlib.Order.Filter.Pointwise
/-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
multiplicative action on `Filter β`.  -/
Filter.distribMulActionFilter : {α : Type u_2} →
  {β : Type u_3} → [inst : Monoid α] → [inst_1 : AddMonoid β] → [DistribMulAction α β] → DistribMulAction α (Filter β)
-- Std.Time.Format.Modifier
/-- `K`: Hour of AM/PM (0-11) (e.g., 0).
 -/
Std.Time.Modifier.K : Std.Time.Number → Std.Time.Modifier
-- Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer
/-- The subgroup `lineStab (span F {v})` is commutative when `v ≠ 0`.  -/
Matrix.SpecialLinearGroup.lineStab_isMulCommutative_of_span' : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (v : ι → F),
  v ≠ 0 →
    ∀ (A B : Matrix.SpecialLinearGroup ι F),
      A ∈ Matrix.SpecialLinearGroup.lineStab (F ∙ v) → B ∈ Matrix.SpecialLinearGroup.lineStab (F ∙ v) → A * B = B * A
-- Mathlib.LinearAlgebra.Eigenspace.Basic
LinearMap.domRestrict.eq_1 : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M), f.domRestrict p = f ∘ₛₗ p.subtype
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.toEquiv_homeomorph : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → TopologicalSpace (β i)],
  (PiLp.homeomorph p β).toEquiv = WithLp.equiv p ((i : ι) → β i)
-- Mathlib.Order.SuccPred.Archimedean
IsSuccArchimedean.mk : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : SuccOrder α],
  (∀ {a b : α}, a ≤ b → ∃ n, Order.succ^[n] a = b) → IsSuccArchimedean α
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_add_of_degree_eq : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p.degree = q.degree → p.leadingCoeff + q.leadingCoeff ≠ 0 → (p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff
-- Mathlib.Algebra.GroupWithZero.Action.Defs
instSMulZeroClass : {α : Type u_10} →
  {β : Type u_11} → [inst : Group α] → [inst_1 : GroupWithZero β] → [MulDistribMulAction α β] → SMulZeroClass α β
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_eq_measure_of_between_null_sdiff`. -/
MeasureTheory.measure_eq_measure_of_between_null_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α},
  s₁ ⊆ s₂ → s₂ ⊆ s₃ → μ (s₃ \ s₁) = 0 → μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.Context.recMap : Lean.Meta.SizeOfSpecNested.Context → Lean.NameMap Lean.Name
-- Mathlib.Algebra.Ring.Ext
NonUnitalCommSemiring.toNonUnitalSemiring_injective : ∀ {R : Type u}, Function.Injective (@NonUnitalCommSemiring.toNonUnitalSemiring R)
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
MonoidAlgebra.instIsDomainOfIsCancelAddOfUniqueProds : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [IsCancelAdd R] [IsDomain R] [inst_3 : Monoid A] [UniqueProds A],
  IsDomain (MonoidAlgebra R A)
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.closure_induction_left : ∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M} {motive : (m : M) → m ∈ AddSubmonoid.closure s → Prop},
  motive 0 ⋯ →
    (∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ AddSubmonoid.closure s), motive y hy → motive (x + y) ⋯) →
      ∀ {x : M} (h : x ∈ AddSubmonoid.closure s), motive x h
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.Edge.map_associator_hom : ∀ {X Y Z : SSet.Truncated 2}
  {x x' : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₁ : SSet.Truncated.Edge x x')
  {y y' : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₂ : SSet.Truncated.Edge y y')
  {z z' : Z.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₃ : SSet.Truncated.Edge z z'),
  ((e₁.tensor e₂).tensor e₃).map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = e₁.tensor (e₂.tensor e₃)
-- Mathlib.Algebra.Group.Submonoid.Operations
MulEquiv.submonoidMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (e : M ≃* N) (S : Submonoid M),
  e.submonoidMap S = { toEquiv := (↑e).image ↑S, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.kernelUnopUnop_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  (CategoryTheory.kernelUnopUnop g).hom =
    (CategoryTheory.Limits.cokernel.desc g (CategoryTheory.Limits.kernel.ι g.unop).op ⋯).unop
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorμ_natural_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (Z₁ Z₂ : C) {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂))
      (CategoryTheory.MonoidalCategory.tensorμ Z₁ Z₂ Y₁ Y₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ Z₁ Z₂ X₁ X₂)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z₁ f₁)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z₂ f₂))
-- Lean.Data.Format
Lean.Std.Format.format.indent : Lean.Option ℕ
-- Mathlib.Analysis.Normed.Module.Normalize
NormedSpace.normalize_eq_zero_iff : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] (x : V), NormedSpace.normalize x = 0 ↔ x = 0
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddLeftCancelSemigroup : {α : Type u_1} → [AddLeftCancelSemigroup α] → AddLeftCancelSemigroup (Lex α)
-- Mathlib.Data.Multiset.Defs
/-- `Pairwise r m` states that there exists a list of the elements s.t. `r` holds pairwise on this
list.  -/
Multiset.Pairwise : {α : Type u_1} → (α → α → Prop) → Multiset α → Prop
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.mem_normalizer_iff_conj_image_eq : ∀ {G : Type u_1} [inst : Group G] {s : Set G} {g : G}, g ∈ Subgroup.normalizer s ↔ ⇑(MulAut.conj g) '' s = s
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G) (c : CategoryTheory.Limits.Cocone F)
  (d : CategoryTheory.Limits.Cocone G) (w : (CategoryTheory.Limits.Cocone.precompose α.inv).obj c ≅ d),
  CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso α c d w =
    (CategoryTheory.Limits.IsColimit.precomposeInvEquiv α c).symm.trans
      (CategoryTheory.Limits.IsColimit.equivIsoColimit w)
-- Mathlib.CategoryTheory.Localization.Composition
CategoryTheory.Functor.IsLocalization.of_comp : ∀ {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₃]
  (L₁ : CategoryTheory.Functor C₁ C₂) (L₂ : CategoryTheory.Functor C₂ C₃) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) (W₃ : CategoryTheory.MorphismProperty C₁) [L₁.IsLocalization W₁]
  [(L₁.comp L₂).IsLocalization W₃], W₁ ≤ W₃ → W₂ = W₃.map L₁ → L₂.IsLocalization W₂
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.pow_inter_pow : ∀ {G : Type u_1} [inst : Group G] {A B : Set G} {K L : ℝ} {m n : ℕ},
  IsApproximateSubgroup K A →
    IsApproximateSubgroup L B →
      2 ≤ m → 2 ≤ n → IsApproximateSubgroup (K ^ (2 * m - 1) * L ^ (2 * n - 1)) (A ^ m ∩ B ^ n)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.comp_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {X Y Z : CategoryTheory.CostructuredArrow S T} (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : C} (h : Z.left ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).left h =
    CategoryTheory.CategoryStruct.comp f.left (CategoryTheory.CategoryStruct.comp g.left h)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Power.denote.match_3.splitter : (motive : Lean.Grind.CommRing.Power → Sort u_1) →
  (x : Lean.Grind.CommRing.Power) → ((x : Lean.Grind.CommRing.Var) → (k : ℕ) → motive { x := x, k := k }) → motive x
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of the reverse direction of `LinearMap.isProj_range_iff_isIdempotentElem`. -/
LinearMap.IsIdempotentElem.isProj_range : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] (f : M →ₗ[S] M),
  IsIdempotentElem f → LinearMap.IsProj f.range f
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.Indep.insert_isCircuit_of_forall_of_nontrivial : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {e : α},
  M.Indep I → I.Nontrivial → e ∈ M.closure I → (∀ f ∈ I, e ∉ M.closure (I \ {f})) → M.IsCircuit (insert e I)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.coe_mul : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (f g : P →ᵃⁱ[𝕜] P),
  ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
LieAlgebra.instLieRingCommutatorRing : (L : Type v) → [LieRing L] → LieRing (CommutatorRing L)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.is_left_invariant_chaar : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G),
  MeasureTheory.Measure.haar.chaar K₀ (TopologicalSpace.Compacts.map (fun x => g * x) ⋯ K) =
    MeasureTheory.Measure.haar.chaar K₀ K
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_eq_ramificationIdx : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [IsDomain R] [IsDedekindDomain S] [Module.IsTorsionFree R S] [q.LiesOver p] [hq : q.IsPrime],
  p ≠ ⊥ → p.ramificationIdx' q = q.ramificationIdx R
-- Mathlib.Topology.Algebra.Order.Field
inv_nhdsLT_zero : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], (nhdsWithin 0 (Set.Iio 0))⁻¹ = Filter.atBot
-- Lean.Meta.Transform
Lean.TransformStep.done.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Lean.TransformStep.done e) = 1 + sizeOf e
-- Lean.Server.FileWorker.SignatureHelp
/-- Stop the search through a syntax stack.  -/
Lean.Server.FileWorker.SignatureHelp.SearchControl.stop : Lean.Server.FileWorker.SignatureHelp.SearchControl
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_1.congr_eq_1 : ∀ {n : ℕ} (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool → Sort u_1)
  (x : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool)
  (h_1 :
    (fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) → (checkSuccess : Bool) → motive (fst, checkSuccess))
  (fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (checkSuccess : Bool),
  x = (fst, checkSuccess) →
    (match x with
      | (fst, checkSuccess) => h_1 fst checkSuccess) ≍
      h_1 fst checkSuccess
-- Lean.Declaration
Lean.mkTheoremValEx : Lean.Name → List Lean.Name → Lean.Expr → Lean.Expr → List Lean.Name → Lean.TheoremVal
-- Mathlib.Data.Complex.Basic
Complex.div_ofNat_re : ∀ (z : ℂ) (n : ℕ) [inst : n.AtLeastTwo], (z / OfNat.ofNat n).re = z.re / OfNat.ofNat n
-- Mathlib.Data.PFun
PFun.core_res : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β), (PFun.res f s).core t = sᶜ ∪ f ⁻¹' t
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_real_ball_center : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (x : E) (r : ℝ), μ.real (Metric.ball x r) = μ.real (Metric.ball 0 r)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.getKey_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (hk : k ∈ m₁) (h : m₁.Equiv m₂),
  m₁.getKey k hk = m₂.getKey k ⋯
-- Init.Core
/-- Auxiliary type used to compile `do` notation. It is an optimization of
`DoResultPRBC PEmpty PEmpty σ` to remove the impossible cases,
used when neither `pure` nor `return` are possible exit paths.
 -/
DoResultBC : Type u → Type u
-- Mathlib.Analysis.Normed.MulAction
/-- For a normed division ring, a sub-multiplicative norm is actually strictly multiplicative.

This is not an instance as it forms a loop with `NormSMulClass.toIsBoundedSMul`.  -/
NormedDivisionRing.toNormSMulClass : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedDivisionRing α] [inst_1 : SeminormedAddGroup β]
  [inst_2 : MulActionWithZero α β] [IsBoundedSMul α β], NormSMulClass α β
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.delete : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Array ℕ → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- `Finsupp.linearCombinationOn M v s` interprets `p : α →₀ R` as a linear combination of a
subset of the vectors in `v`, mapping it to the span of those vectors.

The subset is indicated by a set `s : Set α` of indices.
 -/
Finsupp.linearCombinationOn : (α : Type u_1) →
  (M : Type u_2) →
    (R : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            (v : α → M) → (s : Set α) → ↥(Finsupp.supported R R s) →ₗ[R] ↥(Submodule.span R (v '' s))
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_rev : ∀ {n : ℕ} {α : Sort u_3} (i : Fin (n + 1)) (a : α) (f : Fin n → α) (j : Fin (n + 1)),
  i.insertNth a f j.rev = i.rev.insertNth a (f ∘ Fin.rev) j
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
posTangentConeAt_mono : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a : E}, Monotone fun s => posTangentConeAt s a
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivWithinAt_one : ∀ {𝕜 : 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 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : One F] (x : E) (s : Set E), HasFDerivWithinAt 1 0 s x
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Submodule.instFiniteDimensionalSubtypeMemComapOfKer : ∀ {K : Type u} {V : Type v} {W : Type v'} [inst : DivisionRing K] [inst_1 : AddCommGroup W] [inst_2 : AddCommGroup V]
  [inst_3 : Module K V] [inst_4 : Module K W] {f : V →ₗ[K] W} (p : Submodule K W) [FiniteDimensional K ↥p]
  [FiniteDimensional K ↥f.ker], FiniteDimensional K ↥(Submodule.comap f p)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.union m₂ ⋯ ⋯).getKey! k = m₂.getKey! k
-- Mathlib.Order.Hom.Bounded
/-- The function preserves the top element. The preferred spelling is `map_top`.  -/
BoundedOrderHom.map_top' : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (self : BoundedOrderHom α β), self.toFun ⊤ = ⊤
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_top_right : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.IsComplement' ⊤ ↔ H = ⊥
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.subset_sdiff`. -/
Set.subset_diff : ∀ {α : Type u_1} {s t u : Set α}, s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.ε₂_ε₁ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] {i₁ i₁' : I₁} {i₂ i₂' : I₂},
  c₁.Rel i₁ i₁' →
    c₂.Rel i₂ i₂' → c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.ε₁ c₂ c₁₂ (i₁, i₂') = -c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.ε₂ c₂ c₁₂ (i₁', i₂)
-- Mathlib.Data.Finsupp.Single
Equiv.finsuppUnique_symm_apply_support_val : ∀ {M : Type u_5} [inst : Zero M] {ι : Type u_13} [inst_1 : Unique ι] (a : M),
  (Equiv.finsuppUnique.symm a).support.val =
    Multiset.map (⇑(Function.Embedding.subtype fun x => x ∈ Function.support (uniqueElim a))) Finset.univ.val
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The identity morphism on an additive monoid object.  -/
CategoryTheory.AddMon.id : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (M : CategoryTheory.AddMon C) → M.Hom M
-- Mathlib.CategoryTheory.Noetherian
CategoryTheory.Noetherian.isNoetherianObject : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Noetherian C] (X : C),
  CategoryTheory.IsNoetherianObject X
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.get_StateT : ∀ {m : Type u → Type v} {psm : Std.Do.PostShape} {σ : Type u} {Q : Std.Do.PostCond σ (Std.Do.PostShape.arg σ psm)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m psm], ⦃fun s => Q.1 s s⦄ MonadStateOf.get ⦃Q⦄
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.mem_map : ∀ {α : Type u} {β : Type v} {m : α → β} {f : Ultrafilter α} {s : Set β}, s ∈ Ultrafilter.map m f ↔ m ⁻¹' s ∈ f
-- Mathlib.Geometry.Euclidean.Triangle
/-- In a parallelogram, the two parts of the inner angle add to the inner angle,
vector angle form.  -/
InnerProductGeometry.angle_eq_angle_add_add_angle_add : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x : V) {y : V},
  y ≠ 0 → InnerProductGeometry.angle x y = InnerProductGeometry.angle x (x + y) + InnerProductGeometry.angle y (x + y)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.neg_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f : X → E} {μ : MeasureTheory.VectorMeasure X F}, μ.Integrable f → (-μ).Integrable f
-- Mathlib.Data.Multiset.ZeroCons
Multiset.Rel.below.cons : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop}
  {motive : (a : Multiset α) → (a_1 : Multiset β) → Multiset.Rel r a a_1 → Prop} {a : α} {b : β} {as : Multiset α}
  {bs : Multiset β} (a_1 : r a b) (a_2 : Multiset.Rel r as bs),
  Multiset.Rel.below a_2 → motive as bs a_2 → Multiset.Rel.below ⋯
-- Mathlib.Combinatorics.SetFamily.Shatter
/-- A set family `𝒜` shatters a set `s` if all subsets of `s` can be obtained as the intersection
of `s` and some element of the set family, and we denote this `𝒜.Shatters s`. We also say that `s`
is *traced* by `𝒜`.  -/
Finset.Shatters : {α : Type u_1} → [DecidableEq α] → Finset (Finset α) → Finset α → Prop
-- Mathlib.Order.Hom.Bounded
BotHom.dual.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : OrderBot α] [inst_2 : LE β] [inst_3 : OrderBot β],
  BotHom.dual =
    { toFun := fun f => { toFun := ⇑f, map_top' := ⋯ }, invFun := fun f => { toFun := ⇑f, map_bot' := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.sub : {α : Type u} → [Div α] → Sub (Additive α)
-- Mathlib.RingTheory.ZariskisMainTheorem
/-- Use `not_isStronglyTranscendental_of_quasiFiniteAt` below instead.  -/
_private.Mathlib.RingTheory.ZariskisMainTheorem.0.Algebra.not_isStronglyTranscendental_of_weaklyQuasiFiniteAt_of_isIntegrallyClosed : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [FaithfulSMul R S]
  [IsIntegrallyClosed R] [IsDomain S] {x : S},
  (Polynomial.aeval x).Finite →
    ∀ (P : Ideal S) [inst_6 : P.IsPrime] [Algebra.WeaklyQuasiFiniteAt R P], ¬IsStronglyTranscendental R x
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stepAux.match_1.eq_6 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4}
  (motive : Turing.TM2.Stmt Γ Λ σ → σ → ((k : K) → List (Γ k)) → Sort u_5) (f : σ → Λ) (v : σ)
  (S : (k : K) → List (Γ k))
  (h_1 :
    (k : K) →
      (f : σ → Γ k) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.push k f q) v S)
  (h_2 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.peek k f q) v S)
  (h_3 :
    (k : K) →
      (f : σ → Option (Γ k) → σ) →
        (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.pop k f q) v S)
  (h_4 :
    (a : σ → σ) →
      (q : Turing.TM2.Stmt Γ Λ σ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.load a q) v S)
  (h_5 :
    (f : σ → Bool) →
      (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) →
        (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.branch f q₁ q₂) v S)
  (h_6 : (f : σ → Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive (Turing.TM2.Stmt.goto f) v S)
  (h_7 : (v : σ) → (S : (k : K) → List (Γ k)) → motive Turing.TM2.Stmt.halt v S),
  (match Turing.TM2.Stmt.goto f, v, S with
    | Turing.TM2.Stmt.push k f q, v, S => h_1 k f q v S
    | Turing.TM2.Stmt.peek k f q, v, S => h_2 k f q v S
    | Turing.TM2.Stmt.pop k f q, v, S => h_3 k f q v S
    | Turing.TM2.Stmt.load a q, v, S => h_4 a q v S
    | Turing.TM2.Stmt.branch f q₁ q₂, v, S => h_5 f q₁ q₂ v S
    | Turing.TM2.Stmt.goto f, v, S => h_6 f v S
    | Turing.TM2.Stmt.halt, v, S => h_7 v S) =
    h_6 f v S
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.ker_toLin_eq_bot : ∀ {n : Type u_1} [inst : Fintype n] {R : Type u_2} {M : Type u_3} [inst_1 : CommRing R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (b : Module.Basis n R M) [inst_4 : DecidableEq n] (A : Matrix n n R),
  IsUnit A.det → ((Matrix.toLin b b) A).ker = ⊥