mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
/-- Given a Lie-Rinehart algebra  `L` containing a LieRinehart subalgebra `L' ⊆ L`, together with a
Lie module `M` of `L`, we may regard `M` as a Lie module of `L'` by restriction.  -/
LieRinehartSubalgebra.lieModule : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) [inst_3 : LieRingModule L A] [inst_4 : LieRinehartRing A L] (R : Type u_3)
  [inst_5 : CommRing R] [inst_6 : Algebra R A] [inst_7 : LieAlgebra R L] [inst_8 : LieRinehartAlgebra R A L]
  {M : Type u_4} [inst_9 : AddCommGroup M] [inst_10 : LieRingModule L M] [inst_11 : Module R M] [LieModule R L M],
  LieModule R (↥L') M
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.mk.congr_simp : ∀ {aig : Std.Sat.AIG ℕ} (cnf : Std.Sat.CNF ℕ) (cache cache_1 : Std.Sat.AIG.toCNF.Cache✝ aig cnf),
  cache = cache_1 →
    ∀ (inv : Std.Sat.AIG.toCNF.State.Inv✝ aig cnf),
      { cnf := cnf, cache := cache, inv := inv } = { cnf := cnf, cache := cache_1, inv := inv }
-- Init.MetaTypes
Lean.Meta.Command.ReduceConfig.mk.inj : ∀ {types proofs implicits : Bool} {transparency : Lean.Meta.TransparencyMode}
  {smartUnfolding check ignoreStuckTC types_1 proofs_1 implicits_1 : Bool} {transparency_1 : Lean.Meta.TransparencyMode}
  {smartUnfolding_1 check_1 ignoreStuckTC_1 : Bool},
  { types := types, proofs := proofs, implicits := implicits, transparency := transparency,
        smartUnfolding := smartUnfolding, check := check, ignoreStuckTC := ignoreStuckTC } =
      { types := types_1, proofs := proofs_1, implicits := implicits_1, transparency := transparency_1,
        smartUnfolding := smartUnfolding_1, check := check_1, ignoreStuckTC := ignoreStuckTC_1 } →
    types = types_1 ∧
      proofs = proofs_1 ∧
        implicits = implicits_1 ∧
          transparency = transparency_1 ∧
            smartUnfolding = smartUnfolding_1 ∧ check = check_1 ∧ ignoreStuckTC = ignoreStuckTC_1
-- Mathlib.Order.SupClosed
supClosed_sInter : ∀ {α : Type u_3} [inst : SemilatticeSup α] {S : Set (Set α)}, (∀ s ∈ S, SupClosed s) → SupClosed (⋂₀ S)
-- Mathlib.Topology.Neighborhoods
nhds_def' : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), nhds x = ⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), Filter.principal s
-- Mathlib.Order.Lattice
/-- **Alias** of the forward direction of `sup_eq_left`. -/
le_of_sup_eq' : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = a → b ≤ a
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.instIsStableUnderCompositionScheme : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.UniversallyOpen
-- Std.Data.DHashMap.RawDef
Std.DHashMap.Raw.instForInSigmaOfMonad : {α : Type u} → {β : α → Type v} → {m : Type w → Type w'} → [Monad m] → ForIn m (Std.DHashMap.Raw α β) ((a : α) × β a)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.iterM_eq_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} {xs : Vector β n}, xs.iterM m = xs.iterFromIdxM m 0
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.comp_of_injective : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {β : Type u_3} {f : β → M} {g : α → β},
  Function.Injective g → Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport (f ∘ g)
-- Lean.Util.Path
/-- Executes `f` with the corresponding module name for each `.lean` file contained in `dir`.

For example, if `dir` contains `A/B/C.lean`, `f` is called with `A.B.C`.
 -/
Lean.forEachModuleInDir : {m : Type → Type u_1} → [Monad m] → [MonadLiftT IO m] → System.FilePath → (Lean.Name → m PUnit.{1}) → m PUnit.{1}
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_symm_zero : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ], (DirectSum.decompose ℳ).symm 0 = 0
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_one : Ordinal.cof 1 = 1
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.unitLattice_rank : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Module.finrank ℤ ↥(NumberField.Units.unitLattice K) = NumberField.Units.rank K
-- Mathlib.Topology.Semicontinuity.Defs
upperHemicontinuousOn_univ_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  UpperHemicontinuousOn f Set.univ ↔ UpperHemicontinuous f
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- If `P` is a presheaf of types and `π : (i : I) → X i ⟶ B` is a family
of morphisms, this is the map from `P.obj (op B)` to the subtype of compatible
families in `P.obj (op (X i))`.  -/
CategoryTheory.Presieve.Arrows.toCompatible : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type w)) →
      {B : C} →
        {I : Type u_1} →
          {X : I → C} →
            (π : (i : I) → X i ⟶ B) → P.obj (Opposite.op B) → Subtype (CategoryTheory.Presieve.Arrows.Compatible P π)
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.hom_ext : ∀ {X Y : Semigrp} {f g : X ⟶ Y}, Semigrp.Hom.hom f = Semigrp.Hom.hom g → f = g
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsPairSelfAdjoint.eq_1 : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] {I : R →+* R} (B F : M →ₗ[R] M →ₛₗ[I] M₁) (f : M → M),
  B.IsPairSelfAdjoint F f = B.IsAdjointPair F f f
-- Init.Data.Dyadic.Basic
Int.natAbs_emod_two : ∀ (i : ℤ), i.natAbs % 2 = (i % 2).natAbs
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.OfSequence.map.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (x : ℕ → C) (x_1 : (n : ℕ) → x n ⟶ x (n + 1)),
  CategoryTheory.Functor.OfSequence.map x_1 0 1 = fun x => x_1 0
-- Mathlib.Topology.Closure
/-- A set is dense if and only if it has a nonempty intersection with each nonempty open set.  -/
dense_iff_inter_open : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.instEmptyCollection : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → EmptyCollection (Aesop.OrderedHashSet α)
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
HasSum.mul_left : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : TopologicalSpace α] [IsTopologicalSemiring α] {f : ι → α} {a₁ : α} (a₂ : α),
  HasSum f a₁ L → HasSum (fun i => a₂ * f i) (a₂ * a₁) L
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.dense_iff_iUnion_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), Dense s ↔ ∀ r > 0, ⋃ c ∈ s, Metric.ball c r = Set.univ
-- Mathlib.RingTheory.Discriminant
/-- If `K` and `L` are fields and `IsScalarTower R K L`, and `b : ι → L` satisfies
` ∀ i, IsIntegral R (b i)`, then `IsIntegral R (discr K b)`.  -/
Algebra.discr_isIntegral : ∀ {ι : Type w} [inst : DecidableEq ι] [inst_1 : Fintype ι] (K : Type u) {L : Type v} [inst_2 : Field K]
  [inst_3 : Field L] [inst_4 : Algebra K L] [Module.Finite K L] {R : Type z} [inst_6 : CommRing R]
  [inst_7 : Algebra R K] [inst_8 : Algebra R L] [IsScalarTower R K L] {b : ι → L},
  (∀ (i : ι), IsIntegral R (b i)) → IsIntegral R (Algebra.discr K b)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- Any function in `ℒp` can be approximated by a simple function if `p < ∞`.  -/
MeasureTheory.MemLp.exists_simpleFunc_eLpNorm_sub_lt : ∀ {β : Type u_2} [inst : MeasurableSpace β] {p : ENNReal} {E : Type u_7} [inst_1 : NormedAddCommGroup E] {f : β → E}
  {μ : MeasureTheory.Measure β},
  MeasureTheory.MemLp f p μ →
    p ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, MeasureTheory.eLpNorm (f - ⇑g) p μ < ε ∧ MeasureTheory.MemLp (⇑g) p μ
-- Mathlib.Data.List.Defs
/-- An auxiliary function for defining `permutations`. `permutationsAux ts is` is the set of all
permutations of `is ++ ts` that do not fix `ts`.  -/
List.permutationsAux : {α : Type u_1} → List α → List α → List (List α)
-- Init.Data.Option.Attach
Option.attach_guard : ∀ {α : Type u_1} {p : α → Bool} {x : α}, (Option.guard p x).attach = if h : p x = true then some ⟨x, ⋯⟩ else none
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_subset_iff : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f : ι → M} {s : Set ι},
  Function.mulSupport f ⊆ s ↔ ∀ (x : ι), f x ≠ 1 → x ∈ s
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.le_preOmega_self : ∀ (o : Ordinal.{u_1}), o ≤ Ordinal.preOmega o
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.counitForward_val_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)}
  (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (x : F.obj (Opposite.op s)),
  CategoryTheory.OverPresheafAux.YonedaCollection.fst (CategoryTheory.OverPresheafAux.counitForward F s x).val = s.hom
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β},
  k ∈ m₂ → Std.DHashMap.Const.getD (m₁.inter m₂) k fallback = Std.DHashMap.Const.getD m₁ k fallback
-- Mathlib.Algebra.Lie.Solvable
LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (k : ℕ), LieAlgebra.derivedSeries R (↥I) k = LieIdeal.comap I.incl (LieAlgebra.derivedSeriesOfIdeal R L k I)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Const.Equiv.beq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq β]
  [ReflBEq β], m₁.WF → m₂.WF → m₁.Equiv m₂ → (m₁ == m₂) = true
-- Mathlib.Order.Fin.Basic
Fin.strictMono_addNat : ∀ {n : ℕ} (m : ℕ), StrictMono fun x => x.addNat m
-- Mathlib.Topology.QuasiSeparated
QuasiSeparatedSpace.of_isOpenEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [QuasiSeparatedSpace α]
  {f : β → α}, Topology.IsOpenEmbedding f → QuasiSeparatedSpace β
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.symm_ε : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E), P.symm.ε = P.ε⁻¹
-- Batteries.Data.List.Lemmas
List.getElem_zero_findIdxs_eq_findIdx_add : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ} (h : 0 < (List.findIdxs p xs s).length),
  (List.findIdxs p xs s)[0] = List.findIdx p xs + s
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.of_le_enorm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} {ε' : Type u_8}
  [inst : TopologicalSpace ε] [inst_1 : TopologicalSpace ε'] [inst_2 : ContinuousENorm ε] [inst_3 : ContinuousENorm ε']
  {f : α → ε} {g : α → ε'},
  MeasureTheory.MemLp g p μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) → MeasureTheory.MemLp f p μ
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.SimpKind.simpAll.sizeOf_spec : sizeOf Lean.Elab.Tactic.SimpKind.simpAll = 1
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
TopRep.d_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : Ring k] [inst_1 : Group G] [inst_2 : TopologicalSpace k]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G), X.d 0 = TopRep.ofHom X.ρ.coind₁ι
-- Std.Do.WP.Monad
/-- `WP.wp` preserves `pure`.  -/
Std.Do.WPMonad.wp_pure : ∀ {m : Type u → Type v} {ps : outParam Std.Do.PostShape} {inst : Monad m} [self : Std.Do.WPMonad m ps] {α : Type u}
  (a : α), Std.Do.wp (pure a) = pure a
-- Mathlib.Analysis.Seminorm
Seminorm.inf_apply : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p q : Seminorm 𝕜 E) (x : E), (p ⊓ q) x = ⨅ u, p u + q (x - u)
-- Mathlib.Data.NNReal.Defs
Real.le_toNNReal_iff_coe_le : ∀ {r : NNReal} {p : ℝ}, 0 ≤ p → (r ≤ p.toNNReal ↔ ↑r ≤ p)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instPowQuotientNat : {R : Type u_1} → [inst : Add R] → [inst_1 : Monoid R] → (c : RingCon R) → Pow c.Quotient ℕ
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.degree_T : ∀ (R : Type u_1) [inst : CommRing R] [IsDomain R] [NeZero 2] (n : ℤ), (Polynomial.Chebyshev.T R n).degree = ↑n.natAbs
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Context.mk : Lean.Meta.Simp.Context →
  Lean.Meta.Simp.Methods →
    Lean.Grind.Config →
      Option (Array Lean.Meta.Grind.AnchorRef) →
        Bool →
          Bool →
            Lean.Meta.Grind.SplitSource →
              Lean.Meta.Grind.EMatchDiagSource →
                Lean.Meta.Grind.SymbolPriorities →
                  Lean.Meta.Grind.ExtensionStateArray → Bool → Bool → Lean.Meta.Grind.Context
-- Mathlib.Data.Tree.Basic
BinaryTree.left_node_right_eq_self : ∀ {x : BinaryTree Unit}, x ≠ BinaryTree.nil → BinaryTree.node () x.left x.right = x
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.coe_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv], ↑0 = 0
-- Mathlib.Algebra.BigOperators.Associated
Prime.dvd_finsuppProd_iff : ∀ {M₀ : Type u_3} {M : Type u_4} [inst : CommMonoidWithZero M] {f : M₀ →₀ M} {g : M₀ → M → ℕ} {p : ℕ},
  Prime p → (p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a))
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.castNum.match_1.eq_2 : ∀ (motive : Num → Sort u_1) (p : PosNum) (h_1 : Unit → motive Num.zero) (h_2 : (p : PosNum) → motive (Num.pos p)),
  (match Num.pos p with
    | Num.zero => h_1 ()
    | Num.pos p => h_2 p) =
    h_2 p
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_pos' : ∀ {E : Type u_5} [inst : NormedGroup E] {a : E}, 0 < ‖a‖₊ ↔ a ≠ 1
-- Mathlib.Logic.Relator
/-- `(R ⇒ S) f g` means `LiftFun R S f g`.  -/
Relator.«term_⇒_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If `f` is meromorphic, then the divisor of `f ^ n` is `n` times the divisor of `f`.
 -/
MeromorphicOn.divisor_fun_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜},
  MeromorphicOn f U → ∀ (n : ℤ), MeromorphicOn.divisor (fun z => f z ^ n) U = n • MeromorphicOn.divisor f U
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename_eq_subst : ∀ {σ : Type u_1} {τ : Type u_2} (f : σ → τ) [inst : Filter.TendstoCofinite f] {R : Type u_6} [inst_1 : CommRing R]
  (p : MvPowerSeries σ R), (MvPowerSeries.rename f) p = MvPowerSeries.subst (MvPowerSeries.X ∘ f) p
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.recZeroCoe_coe : ∀ {α : Type u} {motive : WithZero α → Sort u_1} (h₁ : motive 0) (h₂ : (a : α) → motive ↑a) (a : α),
  WithZero.recZeroCoe h₁ h₂ ↑a = h₂ a
-- Plausible.Testable
Plausible.TestResult.instToString : {p : Prop} → ToString (Plausible.TestResult p)
-- Mathlib.Algebra.Module.Presentation.Differentials
Algebra.Presentation.differentials.surjective_hom₁ : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (pres : Algebra.Presentation R S ι σ), Function.Surjective ⇑(Algebra.Presentation.differentials.hom₁ pres)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.diamond_aux : ∀ {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool},
  L₁ ++ (x1, b1) :: (x1, !b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, !b2) :: L₄ →
    L₁ ++ L₂ = L₃ ++ L₄ ∨ ∃ L₅, FreeAddGroup.Red.Step (L₁ ++ L₂) L₅ ∧ FreeAddGroup.Red.Step (L₃ ++ L₄) L₅
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.post : Lean.Meta.SimpTheorems → Lean.Meta.SimpTheoremTree
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_mul : ∀ (a b : UInt16), (a * b).toUInt32 = a.toUInt32 * b.toUInt32 % 65536
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpParams : Type
-- Mathlib.Algebra.Module.End
AddMonoid.End.intCast_def : ∀ (M : Type u_3) [inst : AddCommGroup M] (z : ℤ), ↑z = (DistribMulAction.toAddMonoidEnd ℤ M) z
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.orthogonalProjectionFn_norm_sq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (v : E),
  ‖v‖ * ‖v‖ =
    ‖v - Submodule.orthogonalProjectionFn v‖ * ‖v - Submodule.orthogonalProjectionFn v‖ +
      ‖Submodule.orthogonalProjectionFn v‖ * ‖Submodule.orthogonalProjectionFn v‖
-- Mathlib.GroupTheory.Index
Subgroup.index_eq_card : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.index = Nat.card (G ⧸ H)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.map : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α β : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  (f : α → β) (x : m α) (Q : Std.Do.PostCond β ps),
  (Std.Do.wp (f <$> x)).apply Q = (Std.Do.wp x).apply (fun a => Q.1 (f a), Q.2)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.functorOfPredicateSet_obj : ∀ {α : PartOrdEmb} (P : Set ↑α → Prop) (J : Subtype P),
  (PartOrdEmb.functorOfPredicateSet P).obj J = { carrier := ↑↑J, str := Subtype.partialOrder fun x => x ∈ ↑J }
-- Mathlib.Data.Vector.Basic
/-- For an index `i : Fin n`, the nth element of `scanl` of a
vector `v : Vector α n` at `i.succ`, is equal to the application
function `f : β → α → β` of the `castSucc i` element of
`scanl f b v` and `get v i`.

This lemma is the `get` version of `scanl_cons`.
 -/
List.Vector.scanl_get : ∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) (v : List.Vector α n) (i : Fin n),
  (List.Vector.scanl f b v).get i.succ = f ((List.Vector.scanl f b v).get i.castSucc) (v.get i)
-- Mathlib.Algebra.Homology.QuasiIso
isoOfQuasiIsoAt_hom_inv_id_assoc : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : QuasiIsoAt f i] {Z : C}
  (h : K.homology i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap f i)
      (CategoryTheory.CategoryStruct.comp (isoOfQuasiIsoAt f i).inv h) =
    h
-- Lean.Syntax
Lean.SyntaxNode.getArg : Lean.SyntaxNode → ℕ → Lean.Syntax
-- Mathlib.Tactic.FunProp.Theorems
/-- Type and important argument of the theorem.  -/
Mathlib.Meta.FunProp.LambdaTheorem.thmArgs : Mathlib.Meta.FunProp.LambdaTheorem → Mathlib.Meta.FunProp.LambdaTheoremArgs
-- Mathlib.RingTheory.PowerSeries.Basic
/-- **Alias** of `PowerSeries.coeff_C_of_ne_zero`. -/
PowerSeries.coeff_ne_zero_C : ∀ {R : Type u_1} [inst : Semiring R] {a : R} {n : ℕ}, n ≠ 0 → (PowerSeries.coeff n) (PowerSeries.C a) = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_op_mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, MulOpposite.op '' (s * t) = MulOpposite.op '' t * MulOpposite.op '' s
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_of_notMem_range : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β} (x : α →₀ M),
  ∀ a ∉ Set.range f, (Finsupp.mapDomain f x) a = 0
-- Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Ideal.isRadical_iff_quotient_reduced : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), I.IsRadical ↔ IsReduced (R ⧸ I)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.BinaryRefVec w → Std.Sat.AIG.RefVecEntry α w
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m m_1 : Std.DHashMap.Raw α β), m = m_1 → ∀ (a : α), m.get? a = m_1.get? a
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonOpenNamespace : Lean.ToJson Lean.Lsp.OpenNamespace
-- Lean.Elab.DocString
Lean.Doc.WithSyntax.mk.injEq : ∀ {α : Type u} (val : α) (stx : Lean.Syntax) (val_1 : α) (stx_1 : Lean.Syntax),
  ({ val := val, stx := stx } = { val := val_1, stx := stx_1 }) = (val = val_1 ∧ stx = stx_1)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.inf_toSubmodule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (K K' : LieSubalgebra R L), (K ⊓ K').toSubmodule = K.toSubmodule ⊓ K'.toSubmodule
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.interior_ssubset_closedInterior : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] [ZeroLEOneClass k] {n : ℕ} (s : Affine.Simplex k P n),
  s.interior ⊂ s.closedInterior
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addRightCancelMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : SMul ℕ M₁]
  [inst_3 : AddRightCancelMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0)
  (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x),
  Function.Injective.addRightCancelMonoid f hf one mul npow =
    { toAddMonoid := Function.Injective.addMonoid f hf one mul npow, toIsRightCancelAdd := ⋯ }
-- Init.Data.Option.Attach
Option.attach_eq_some_iff : ∀ {α : Type u_1} {o : Option α} {x : { x // o = some x }}, o.attach = some x ↔ o = some ↑x
-- Mathlib.Algebra.Group.Action.Faithful
faithfulSMul_iff : ∀ {G : Type u_2} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α],
  FaithfulSMul G α ↔ ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
-- Mathlib.Order.Filter.Defs
/-- A function `f` is eventually less than or equal to a function `g` at a filter `l`.  -/
Filter.«term_≤ᶠ[_]_» : Lean.TrailingParserDescr
-- Std.Do.WP.Sound
/-- From a `wp`-provable postcondition and an `Internal.MayReturn` witness, conclude `P`
at that value.
 -/
Std.Do.WPSound.of_wp : ∀ {m : Type u → Type u_1} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WP m ps] [Std.Do.WPSound m ps]
  {α : Type u} {x : m α} {a : α} {P : α → Prop},
  Std.Do.Internal.MayReturn x a → (⊢ₛ (Std.Do.wp x).apply (Std.Do.PostCond.mayThrow fun a => ⌜P a⌝)) → P a
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.of.sizeOf_spec : ∀ (carrier : Type u) [str : MeasurableSpace carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.ofRepresentableBy.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  (F : CategoryTheory.Functor Cᵒᵖ AddGrpCat) (α : (F.comp (CategoryTheory.forget AddGrpCat)).RepresentableBy X),
  CategoryTheory.AddGrpObj.ofRepresentableBy X F α =
    {
      toAddMonObj :=
        CategoryTheory.AddMonObj.ofRepresentableBy X (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat)) α,
      neg := α.homEquiv'.symm (-α.homEquiv (CategoryTheory.CategoryStruct.id X)), left_neg := ⋯, right_neg := ⋯ }
-- Init.Data.Ord.Basic
List.isLE_compare_nil_right : ∀ {α : Type u_1} [inst : Ord α] {xs : List α}, (compare xs []).isLE = true ↔ xs = []
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns a `List` of the key/value pairs in order.  -/
Std.DTreeMap.Internal.Impl.toList : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → List ((a : α) × β a)
-- Mathlib.Data.PNat.Notation
coePNatNat : Coe ℕ+ ℕ