mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : C ⥤ D` preserves
colimits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.preservesColimit_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit K.op F.op],
  CategoryTheory.Limits.PreservesColimit K F
-- Mathlib.Data.Nat.Totient
Nat.totient_two : Nat.totient 2 = 1
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.zipWithLeft'.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (bs : List β) (h_1 : (bs : List β) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → motive (a :: as) [])
  (h_3 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs)),
  (match [], bs with
    | [], bs => h_1 bs
    | a :: as, [] => h_2 a as
    | a :: as, b :: bs => h_3 a as b bs) =
    h_1 bs
-- Lean.Parser.Term
Lean.Parser.Termination.inductiveFixpoint.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.small_of_hasSmallLocalizedHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [L.IsLocalization W] (X Y : C)
  [CategoryTheory.Localization.HasSmallLocalizedHom W X Y], Small.{w, v₂} (L.obj X ⟶ L.obj Y)
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.order_toSubring : ∀ {R : Type u_1} [inst : Ring R] (p : PowerSeries R) (T : Subring R) (hp : ∀ (n : ℕ), (PowerSeries.coeff n) p ∈ T),
  (p.toSubring T hp).order = p.order
-- Mathlib.Order.Filter.Cofinite
/-- For natural numbers the filters `Filter.cofinite` and `Filter.atTop` coincide.  -/
Nat.cofinite_eq_atTop : Filter.cofinite = Filter.atTop
-- Mathlib.Analysis.Complex.Exponential
/-- The real exponential function, defined as the real part of the complex exponential  -/
Real.exp : ℝ → ℝ
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.HomologySequence.δ_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : autoParam (n₀ + 1 = n₁) DerivedCategory.HomologySequence.δ_comp._auto_1),
      CategoryTheory.CategoryStruct.comp (DerivedCategory.HomologySequence.δ T n₀ n₁ h)
          ((DerivedCategory.homologyFunctor C n₁).map T.mor₁) =
        0
-- Mathlib.Order.Hom.Basic
OrderEmbedding.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (f : α ↪o β), (OrderEmbedding.id α).comp f = f
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.ShiftMkCore.shiftFunctor_eq : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (h : CategoryTheory.ShiftMkCore C A) (a : A), CategoryTheory.shiftFunctor C a = h.F a
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instHasPushoutsOfHasPushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C)
  [CategoryTheory.Limits.HasPushouts C], P.HasPushouts
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
_private.Mathlib.AlgebraicTopology.SimplicialSet.Degenerate.0.SSet.unique_nonDegenerate.le : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := n })} {m₁ m₂ : ℕ} {f₁ : { len := n } ⟶ { len := m₁ }}
  (hf₁ : CategoryTheory.SplitEpi f₁) {y₁ : ↑(X.nonDegenerate m₁)},
  x = (CategoryTheory.ConcreteCategory.hom (X.map f₁.op)) ↑y₁ →
    ∀ {f₂ : { len := n } ⟶ { len := m₂ }} {y₂ : X.obj (Opposite.op { len := m₂ })},
      x = (CategoryTheory.ConcreteCategory.hom (X.map f₂.op)) y₂ → m₁ ≤ m₂
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.mapKer_apply_coe : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] (f : P.Hom P')
  [alg : Algebra P.Ring P'.Ring] (halg : algebraMap P.Ring P'.Ring = f.toRingHom) (x : ↥P.ker),
  ↑((f.mapKer halg) x) = f.toRingHom ↑x
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries`.

---

The lower central series of a subgroup `S` of `G`, computed in the ambient group `G`.
This is the iterated commutator `⁅⁅⋯⁅S, S⁆, S⁆⋯, S⁆`, a subgroup of `G`. The lower central series
of `G` itself is the case `S = ⊤`.  -/
lowerCentralSeries : {G : Type u_1} → [inst : Group G] → Subgroup G → ℕ → Subgroup G
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.trimmed : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α), μ.trim = μ.toOuterMeasure
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.unopEquiv_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) (l : sq.LiftStruct),
  (CategoryTheory.CommSq.LiftStruct.unopEquiv sq) l = l.unop
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- When the first map `S.f` is zero, this is the left homology data on `S` given
by the chosen `kernel S.g`  -/
CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [CategoryTheory.Limits.HasKernel S.g] → S.f = 0 → S.LeftHomologyData
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.add_zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Mathlib.Order.LatticeIntervals
Set.Iic.semilatticeSup : {α : Type u_1} → {a : α} → [inst : SemilatticeSup α] → SemilatticeSup ↑(Set.Iic a)
-- Mathlib.Order.RelIso.Basic
RelIso.apply_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (x : β), e (e.symm x) = x
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projection_eq_self_iff`.

---

The projection to `p` along `q` of `x` equals `x` if and only if `x ∈ p`.  -/
Submodule.IsCompl.projection_eq_self_iff : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E), (p.projection q hpq) x = x ↔ x ∈ p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keysArray_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.Internal.Impl.map f t).keysArray = t.keysArray
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The constructed binary fan is indeed a limit  -/
TopCat.prodBinaryFanIsLimit : (X Y : TopCat) → CategoryTheory.Limits.IsLimit (X.prodBinaryFan Y)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensOptions.mk.sizeOf_spec : ∀ (legend : Lean.Lsp.SemanticTokensLegend) (range full : Bool),
  sizeOf { legend := legend, range := range, full := full } = 1 + sizeOf legend + sizeOf range + sizeOf full
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.CombinatorAttribute.impl : Lean.ParserCompiler.CombinatorAttribute → Lean.AttributeImpl
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.of_isEmpty : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [IsEmpty α] {f : α → β}, MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.Topology.Compactness.SigmaCompact
IsSigmaCompact.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X),
  IsSigmaCompact s = ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = s
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- The conjugation action by elements of the Lipschitz group keeps vectors as vectors.  -/
lipschitzGroup.conjAct_smul_ι_mem_range_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ},
  x ∈ lipschitzGroup Q →
    ∀ [Invertible 2] (m : M), ConjAct.toConjAct x • (CliffordAlgebra.ι Q) m ∈ (CliffordAlgebra.ι Q).range
-- Mathlib.Algebra.Order.Floor.Defs
Int.floor_nonneg : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a : α}, 0 ≤ ⌊a⌋ ↔ 0 ≤ a
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.mul_lt_const : ∀ {α : Type u_1} {b c : α} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α],
  b < c → ∀ {a : α}, 0 < a → b * a < c * a
-- Mathlib.MeasureTheory.Measure.Restrict
IsCountablySpanning.null_of_forall_inter_null : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {C : Set (Set α)},
  IsCountablySpanning C → (∀ t ∈ C, μ (s ∩ t) = 0) → μ s = 0
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.prime : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R), Prime v.asIdeal
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_to_inv : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M), ↑(extChartAt I x).symm (↑(extChartAt I x) x) = x
-- Mathlib.Topology.Category.Sequential
/-- The fully faithful embedding of `Sequential` in `TopCat`.  -/
Sequential.sequentialToTop : CategoryTheory.Functor Sequential TopCat
-- Mathlib.Order.RelIso.Set
Subrel.instIsTransSubtype : ∀ {α : Type u_1} (r : α → α → Prop) [IsTrans α r] (p : α → Prop), IsTrans (Subtype p) (Subrel r p)
-- Lean.Level
Lean.Level.isParam : Lean.Level → Bool
-- Mathlib.Algebra.Order.CompleteField
/-- The lower cut of rationals inside a linear ordered field that are less than a given element of
another linear ordered field.  -/
LinearOrderedField.cutMap : {α : Type u_2} → (β : Type u_3) → [Field α] → [LinearOrder α] → [DivisionRing β] → α → Set β
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.continuous_sin : Continuous Real.Angle.sin
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
Seminorm.bound_comp_of_isInducing : ∀ {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [inst : AddCommGroup E] [inst_1 : NormedField 𝕜₂]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜₂ F] [inst_4 : TopologicalSpace F] {𝕜 : Type u_11}
  [inst_5 : NontriviallyNormedField 𝕜] [inst_6 : Module 𝕜 E] [inst_7 : TopologicalSpace E] {σ₁₂ : 𝕜 →+* 𝕜₂}
  [inst_8 : RingHomIsometric σ₁₂] {p : Seminorm 𝕜 E},
  Continuous ⇑p →
    ∀ {q : SeminormFamily 𝕜₂ F ι},
      WithSeminorms q → ∀ {f : E →ₛₗ[σ₁₂] F}, Topology.IsInducing ⇑f → ∃ s C, C ≠ 0 ∧ p ≤ (C • s.sup q).comp f
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacksAlong : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Limits.HasPullbacksAlong f], P.HasPullbacksAlong f
-- Mathlib.Data.Nat.Choose.Central
Nat.two_dvd_centralBinom_succ : ∀ (n : ℕ), 2 ∣ (n + 1).centralBinom
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_inv_nhdsGT_inv : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousInv H] {a : H}, Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Ioi a⁻¹)) (nhdsWithin a (Set.Iio a))
-- Mathlib.Topology.Compactness.Compact
/-- **Alias** of the forward direction of `isCompact_iff_ultrafilter_le_nhds`. -/
IsCompact.ultrafilter_le_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ (f : Ultrafilter X), ↑f ≤ Filter.principal s → ∃ x ∈ s, ↑f ≤ nhds x
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.map_comp_ι : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u4}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  (ExteriorAlgebra.map f).toLinearMap ∘ₗ ExteriorAlgebra.ι R = ExteriorAlgebra.ι R ∘ₗ f
-- Mathlib.Analysis.Convex.Combination
Finset.mem_convexHull : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {s : Finset E} {x : E},
  x ∈ (convexHull R) ↑s ↔ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.ret.inj : ∀ {k k_1 : Turing.PartrecToTM2.Cont'}, Turing.PartrecToTM2.Λ'.ret k = Turing.PartrecToTM2.Λ'.ret k_1 → k = k_1
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_neg : ∀ (x : ℝ), Real.cos (-x) = Real.cos x
-- Lean.Language.Basic
Lean.Language.SnapshotLeaf.mk.sizeOf_spec : ∀ (toSnapshot : Lean.Language.Snapshot), sizeOf { toSnapshot := toSnapshot } = 1 + sizeOf toSnapshot
-- Mathlib.Tactic.ProdAssoc
/-- The number of types appearing in an iterated product encoded as a `ProdTree`.  -/
Lean.Expr.ProdTree.size : Lean.Expr.ProdTree → ℕ
-- Mathlib.Analysis.Polynomial.Fourier
/-- The `n`th Fourier coefficient of a polynomial is the coefficient of `X ^ n`  -/
Polynomial.fourierCoeff_toAddCircle_natCast : ∀ (p : Polynomial ℂ) (n : ℕ), fourierCoeff ⇑(Polynomial.toAddCircle p) ↑n = p.coeff n
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_add_supp : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  (a : R) {s : R}, s ∈ v.supp → v (a + s) = v a
-- Init.Data.Nat.Fold
Nat.all_eq_finRange_all : ∀ {n : ℕ} (f : (i : ℕ) → i < n → Bool),
  n.all f =
    (List.finRange n).all fun x =>
      match x with
      | ⟨i, h⟩ => f i h
-- Mathlib.Analysis.Convex.Gauge
gauge_lt_one_iff_mem_interior : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} [inst_2 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], Convex ℝ s → s ∈ nhds 0 → (gauge s x < 1 ↔ x ∈ interior s)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.nonneg_iff_exists_nonneg_and_eq_mul_self : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [StarOrderedRing A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A]
  [T2Space A] {a : A}, 0 ≤ a ↔ ∃ b, 0 ≤ b ∧ a = b * b
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.IsUniform.congr_simp : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ {inst_2 : DecidableRel G.Adj} [inst_3 : DecidableRel G_1.Adj] (ε ε_1 : 𝕜),
      ε = ε_1 →
        ∀ (s s_1 : Finset α), s = s_1 → ∀ (t t_1 : Finset α), t = t_1 → G.IsUniform ε s t = G_1.IsUniform ε_1 s_1 t_1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.constInsertMany! : ∀ {α : Type u} {β : Type v} {x : Ord α} [Std.TransOrd α] {ρ : Type u_1} [inst : ForIn Id ρ (α × β)] {l : ρ}
  {t : Std.DTreeMap.Internal.Impl α fun x => β}, t.WF → (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).WF
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_add_neg : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
  [inst_2 : SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (g h : ι → G), ⇑f ∘ (g + -h) = ⇑f ∘ g + -⇑f ∘ h
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsFixedPt.piMap : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i → α i} {x : (i : ι) → α i},
  (∀ (i : ι), Function.IsFixedPt (f i) (x i)) → Function.IsFixedPt (Pi.map f) x
-- Mathlib.LinearAlgebra.Semisimple
Module.End.isSemisimple_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M}, f.IsSemisimple ↔ ∀ p ∈ f.invtSubmodule, ∃ q ∈ f.invtSubmodule, IsCompl p q
-- Lean.ToExpr
/-- Convert a value `a : α` into an expression that denotes `a`  -/
Lean.ToExpr.toExpr : {α : Type u} → [self : Lean.ToExpr α] → α → Lean.Expr
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The composition of monoid isomorphisms associated to equivalences of additive group
extensions gives another equivalence.  -/
AddGroupExtension.Equiv.trans : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] →
          [inst_2 : AddGroup G] →
            {S : AddGroupExtension N E G} →
              {E' : Type u_4} →
                [inst_3 : AddGroup E'] →
                  {S' : AddGroupExtension N E' G} →
                    S.Equiv S' →
                      {E'' : Type u_5} →
                        [inst_4 : AddGroup E''] → {S'' : AddGroupExtension N E'' G} → S'.Equiv S'' → S.Equiv S''
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.add_sum_Iio_eq_sum_Iic : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → M} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrderBot α] (a : α), f a + ∑ x < a, f x = ∑ x ≤ a, f x
-- Mathlib.Data.Set.Sups
Set.sep_sups_le : ∀ {α : Type u_2} [inst : SemilatticeSup α] (s t : Set α) (a : α),
  {b | b ∈ s ⊻ t ∧ b ≤ a} = {b | b ∈ s ∧ b ≤ a} ⊻ {b | b ∈ t ∧ b ≤ a}
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_comp_eq_of_range_subset : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N] {g : M → N} {f : ι → M},
  (∀ {x : M}, x ∈ Set.range f → (g x = 1 ↔ x = 1)) → Function.mulSupport (g ∘ f) = Function.mulSupport f
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `orthogonal` reverses the `≤` ordering of two
subspaces.  -/
Submodule.orthogonal_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K₁ K₂ : Submodule 𝕜 E}, K₁ ≤ K₂ → K₂ᗮ ≤ K₁ᗮ
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.integral_preCDF_fst : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℚ) [MeasureTheory.IsFiniteMeasure ρ],
  ∫ (x : α), (ProbabilityTheory.preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd ↑r).real Set.univ
-- Mathlib.Analysis.Analytic.Composition
AnalyticAt.comp_analyticWithinAt_of_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {x : E} {y : F} {s : Set E},
  AnalyticAt 𝕜 g y → AnalyticWithinAt 𝕜 f s x → f x = y → AnalyticWithinAt 𝕜 (g ∘ f) s x
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Special case of the standard formula for functions on `ℂ`, with the standard real inner product
structure.
 -/
InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℂ → F),
  Laplacian.laplacian f = fun x => (iteratedFDeriv ℝ 2 f x) ![1, 1] + (iteratedFDeriv ℝ 2 f x) ![Complex.I, Complex.I]
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.Context.mk.injEq : ∀ (pattern : Lean.Meta.Sym.Pattern) (unify zetaDelta : Bool) (pattern_1 : Lean.Meta.Sym.Pattern)
  (unify_1 zetaDelta_1 : Bool),
  ({ pattern := pattern, unify := unify, zetaDelta := zetaDelta } =
      { pattern := pattern_1, unify := unify_1, zetaDelta := zetaDelta_1 }) =
    (pattern = pattern_1 ∧ unify = unify_1 ∧ zetaDelta = zetaDelta_1)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.UniformIntegrable.unifIntegrable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f : ι → α → β} {p : ENNReal},
  MeasureTheory.UniformIntegrable f p μ → MeasureTheory.UnifIntegrable f p μ
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- **Alias** of `FunLike.coeAddMonoidHom`. -/
MultilinearMap.coeAddMonoidHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : AddZero F] → [inst_2 : AddZeroClass β] → [IsZeroApply F α β] → [IsAddApply F α β] → F →+ α → β
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimTargetView.hIdent? : Lean.Elab.Tactic.ElimTargetView → Option Lean.Ident
-- Mathlib.Tactic.Algebra.Basic
Mathlib.Tactic.Algebra.Cache.mk.injEq : ∀ {u : Lean.Level} {A : Q(Type u)} {sA : Q(CommSemiring «$A»)} (toCache : Mathlib.Tactic.Ring.Common.Cache sA)
  (field : Option Q(Field «$A»)) (toCache_1 : Mathlib.Tactic.Ring.Common.Cache sA) (field_1 : Option Q(Field «$A»)),
  ({ toCache := toCache, field := field } = { toCache := toCache_1, field := field_1 }) =
    (toCache = toCache_1 ∧ field = field_1)
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.unit_app_shift_commShiftIso_inv_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A] (a : A)
  (X : C) {Z : C} (h : G.obj (F.obj ((CategoryTheory.shiftFunctor C a).obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map (adj.unit.app X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (F.comp G) a).inv.app X) h) =
    CategoryTheory.CategoryStruct.comp (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj X)) h
-- Batteries.Data.BinomialHeap.Basic
/-- `O(1)`. Is the heap empty?  -/
Batteries.BinomialHeap.isEmpty : {α : Type u} → {le : α → α → Bool} → Batteries.BinomialHeap α le → Bool
-- Std.Do.PostCond
Std.Do.ExceptConds.and_elim_left : ∀ {ps : Std.Do.PostShape} (x y : Std.Do.ExceptConds ps), (x ∧ₑ y).entails x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isSome_get?_eq_contains : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, (Std.DHashMap.Raw.Const.get? m a).isSome = m.contains a
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  [mon : CategoryTheory.MonObj X] (X_1 : C) (mon_1 : CategoryTheory.MonObj X_1),
  ({ X := X, mon := mon } = { X := X_1, mon := mon_1 }) = (X = X_1 ∧ mon ≍ mon_1)
-- Mathlib.Algebra.Star.Subalgebra
/-- If all elements of `s : Set A` commute pairwise and also commute pairwise with elements of
`star s`, then `StarSubalgebra.adjoin R s` is commutative. See note [reducible non-instances].  -/
StarAlgebra.adjoinCommSemiringOfComm : (R : Type u_2) →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : StarRing A] →
              [inst_5 : StarModule R A] →
                {s : Set A} →
                  (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) →
                    (∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) → CommSemiring ↥(StarAlgebra.adjoin R s)