mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.curryMid_apply_apply : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (p : Fin (n + 1)) (f : MultilinearMap R M M₂)
  (x : M p) (m : (i : Fin n) → M (p.succAbove i)), ((MultilinearMap.curryMid p f) x) m = f (p.insertNth x m)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarKind.tactic.inj : ∀ {tacticCode : Lean.Syntax} {ctx : Lean.Elab.Term.SavedContext} {kind : Lean.Elab.Term.TacticMVarKind}
  {delayOnMVars : Bool} {tacticCode_1 : Lean.Syntax} {ctx_1 : Lean.Elab.Term.SavedContext}
  {kind_1 : Lean.Elab.Term.TacticMVarKind} {delayOnMVars_1 : Bool},
  Lean.Elab.Term.SyntheticMVarKind.tactic tacticCode ctx kind delayOnMVars =
      Lean.Elab.Term.SyntheticMVarKind.tactic tacticCode_1 ctx_1 kind_1 delayOnMVars_1 →
    tacticCode = tacticCode_1 ∧ ctx = ctx_1 ∧ kind = kind_1 ∧ delayOnMVars = delayOnMVars_1
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.orthogonal_cross_right : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] {v w : Projectivization F (Fin 3 → F)},
  v ≠ w → w.orthogonal (v.cross w)
-- Init.Data.Nat.Lemmas
Nat.min_left_comm : ∀ (a b c : ℕ), min a (min b c) = min b (min a c)
-- Init.Data.SInt.Lemmas
Int16.zero_mod : ∀ {a : Int16}, 0 % a = 0
-- Mathlib.Algebra.Notation.Lemmas
dite_nonpos : ∀ {α : Type u_1} [inst : Zero α] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α} [inst_2 : LE α],
  (∀ (h : p), a h ≤ 0) → (∀ (h : ¬p), b h ≤ 0) → dite p a b ≤ 0
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_inv : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] (k : K) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j)
        (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).inv) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.obj k) j)
      (CategoryTheory.Limits.colimit.ι (F.flip.comp CategoryTheory.Limits.colim) k)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.integrable_iff : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {f : MeasureTheory.SimpleFunc α E}, MeasureTheory.Integrable (⇑f) μ ↔ ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- Preimages of codiscrete sets, local version: if `f` is analytic at `x` and not locally constant,
then the preimage of any punctured neighbourhood of `f x` is a punctured neighbourhood of `x`.  -/
AnalyticAt.preimage_of_nhdsNE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} {s : Set E},
  AnalyticAt 𝕜 f x → ¬Filter.EventuallyConst f (nhds x) → s ∈ nhdsWithin (f x) {f x}ᶜ → f ⁻¹' s ∈ nhdsWithin x {x}ᶜ
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toList_eq_nil_iff : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α], r.toList = [] ↔ (Std.PRange.succ? r.lower).isNone = true
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.associator_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F G H : CategoryTheory.Functor C D} {X : C},
  (CategoryTheory.MonoidalCategoryStruct.associator F G H).hom.app X =
    (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (G.obj X) (H.obj X)).hom
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
/-- The autoequivalence `Cᵒᵖ ≌ Cᵒᵖ` whose functor is `shiftFunctor Cᵒᵖ n` and whose inverse
functor is `(shiftFunctor C n).op`. In most cases, it is not necessary to unfold the
definitions of the unit and counit isomorphisms: the compatibilities they satisfy
are stated as separate lemmas.  -/
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence : (C : Type u_1) → [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.HasShift C ℤ] → ℤ → (Cᵒᵖ ≌ Cᵒᵖ)
-- Mathlib.Order.Minimal
Maximal.and_left : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : LE α], Maximal P x → Q x → Maximal (fun x => Q x ∧ P x) x
-- Lean.AuxRecursor
Lean.mkBRecOnName : Lean.Name → Lean.Name
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.interior_inter_support : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] {s : Set X}, interior s ∩ μ.support ⊆ (μ.restrict s).support
-- Mathlib.Order.Hom.BoundedLattice
OrderIsoClass.toInfTopHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : SemilatticeInf α]
  [inst_2 : OrderTop α] [inst_3 : SemilatticeInf β] [inst_4 : OrderTop β] [OrderIsoClass F α β], InfTopHomClass F α β
-- Mathlib.RingTheory.LinearDisjoint
/-- If a basis of `B` is also `A`-linearly independent, then `A` and `B` are linearly disjoint.  -/
Subalgebra.LinearDisjoint.of_basis_right : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  {ι : Type u_1} (b : Module.Basis ι R ↥B), LinearIndependent (↥A) (⇑B.val ∘ ⇑b) → A.LinearDisjoint B
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- Spec is a full functor.  -/
AlgebraicGeometry.Spec.full : AlgebraicGeometry.Scheme.Spec.Full
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.ennrealVariation_apply : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ : MeasureTheory.VectorMeasure X V) {s : Set X},
  MeasurableSet s → μ.ennrealVariation s = μ.variation s
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.match_3.splitter : (motive : List Lean.MVarId → Sort u_1) →
  (curr : List Lean.MVarId) →
    (Unit → motive []) → ((g : Lean.MVarId) → (gs : List Lean.MVarId) → motive (g :: gs)) → motive curr
-- Mathlib.Order.Monotone.Basic
/-- If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
monotone function `f : ℤ → α`.  -/
Int.exists_strictMono : ∀ (α : Type u) [inst : Preorder α] [Nonempty α] [NoMinOrder α] [NoMaxOrder α], ∃ f, StrictMono f
-- Mathlib.Topology.ShrinkingLemma
/-- The partially refined family still covers the set.  -/
ShrinkingLemma.PartialRefinement.subset_iUnion : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  (self : ShrinkingLemma.PartialRefinement u s p), s ⊆ ⋃ i, self.toFun i
-- Std.Data.ExtHashMap.Basic
/-- The number of mappings present in the hash map  -/
Std.ExtHashMap.size : {α : Type u} →
  {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → ℕ
-- Mathlib.Topology.Maps.Basic
/-- A map `f : X → Y` is closed if and only if for all sets `s`, any cluster point of `f '' s` is
the image by `f` of some cluster point of `s`.
If you require this for all filters instead of just principal filters, and also that `f` is
continuous, you get the notion of **proper map**. See `isProperMap_iff_clusterPt`.  -/
isClosedMap_iff_clusterPt : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f ↔
    ∀ (s : Set X) (y : Y), MapClusterPt y (Filter.principal s) f → ∃ x, f x = y ∧ ClusterPt x (Filter.principal s)
-- Mathlib.Topology.VectorBundle.Basic
/-- A fiberwise linear map equal to `e` on `e.baseSet`.  -/
Bundle.Trivialization.linearMapAt : (R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : Semiring R] →
          [inst_1 : TopologicalSpace F] →
            [inst_2 : TopologicalSpace B] →
              [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] →
                [inst_4 : AddCommMonoid F] →
                  [inst_5 : Module R F] →
                    [inst_6 : (x : B) → AddCommMonoid (E x)] →
                      [inst_7 : (x : B) → Module R (E x)] →
                        (e : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                          [Bundle.Trivialization.IsLinear R e] → (b : B) → E b →ₗ[R] F
-- Mathlib.Topology.Irreducible
/-- [Stacks Tag 004Z](https://stacks.math.columbia.edu/tag/004Z) -/
IsPreirreducible.preimage_of_dense_isPreirreducible_fiber : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {V : Set Y},
  IsPreirreducible V →
    ∀ (f : X → Y), IsOpenMap f → V ⊆ closure (V ∩ {x | IsPreirreducible (f ⁻¹' {x})}) → IsPreirreducible (f ⁻¹' V)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKey_modifyKey_beq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β} {he : (Std.Internal.List.Const.modifyKey k f l).isEmpty = false},
      (Std.Internal.List.minKey (Std.Internal.List.Const.modifyKey k f l) he == Std.Internal.List.minKey l ⋯) = true
-- Mathlib.Algebra.GroupWithZero.Center
Set.inv_mem_centralizer₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {s : Set G₀} {a : G₀}, a ∈ s.centralizer → a⁻¹ ∈ s.centralizer
-- Mathlib.Condensed.Functors
/-- The yoneda presheaf as an actual condensed set.  -/
compHausToCondensed : CategoryTheory.Functor CompHaus CondensedSet
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_iff_eq_zero_of_smul_mem_span : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M}, LinearIndependent R v ↔ ∀ (i : ι) (a : R), a • v i ∈ Submodule.span R (v '' (Set.univ \ {i})) → a = 0
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm_mono : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s₁ s₂ : Multiset α},
  s₁ ⊆ s₂ → s₁.lcm ∣ s₂.lcm
-- Init.Data.SInt.Lemmas
ISize.toInt_sub_of_le : ∀ (a b : ISize), 0 ≤ b → b ≤ a → (a - b).toInt = a.toInt - b.toInt
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- We call *occurrence set* for pattern `p` and position `g` the set of configurations
in which a pattern `p` occurs at position `g`.

This proves that it is exactly the cylinder corresponding to the
pattern obtained by translating `p` by `g`.

Equivalently, `p.occursInAt x g` iff on every translated site `g + w` (with `w ∈ p.support`)
the configuration `x` agrees with the translated pattern `Pattern.shift p g`.

(This uses `[IsLeftCancelMul G]` to identify the preimage along left-multiplication by `g`.)  -/
SymbolicDynamics.FullShift.occursInAt_eq_cylinder : ∀ {A : Type u_1} [inst : Inhabited A] {G : Type u_2} [inst_1 : AddMonoid G] [IsLeftCancelAdd G]
  (p : SymbolicDynamics.FullShift.Pattern A G) (g : G),
  {x | p.occursInAt x g} = SymbolicDynamics.FullShift.cylinder (Finset.image (fun x => g + x) p.support) (p.shift g)
-- Mathlib.Order.Heyting.Basic
compl_compl_himp_distrib : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a b : α), (a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.self : ∀ {R : Type u} [inst : CommSemiring R], Module.Flat R R
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_add_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  ⌈a + 1⌉ = ⌈a⌉ + 1
-- Mathlib.SetTheory.Ordinal.Family
/-- Converts a family indexed by an `Ordinal.{u}` to one indexed by a `Type u` using a well-ordering
given by the axiom of choice.  -/
Ordinal.familyOfBFamily : {α : Type u_1} → (o : Ordinal.{u_3}) → ((a : Ordinal.{u_3}) → a < o → α) → o.ToType → α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)] {Z_1 : C}
  (h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp f f') g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f' (CategoryTheory.Limits.pushout.inl f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutRightPushoutInlIso f g f').hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp f f') g) h
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.mk.sizeOf_spec : ∀ {α β σ : Type} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ] (descr : Lean.ScopedEnvExtension.Descr α β σ)
  (ext :
    Lean.PersistentEnvExtension (Lean.ScopedEnvExtension.Entry α) (Lean.ScopedEnvExtension.Entry β)
      (Lean.ScopedEnvExtension.StateStack α β σ)),
  sizeOf { descr := descr, ext := ext } = 1 + sizeOf descr + sizeOf ext
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- `𝔸(n; S)` is the affine `n`-space over `S`.
Note that `n : Type u` is an arbitrary index type (e.g. `ULift.{u} (Fin m)`).  -/
AlgebraicGeometry.AffineSpace : Type u → AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme
-- Mathlib.Analysis.PSeries
Finset.sum_condensed_le' : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M},
  (∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) →
    ∀ (n : ℕ), ∑ k ∈ Finset.range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k ∈ Finset.Ico 2 (2 ^ n + 1), f k
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_eq_none : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, a ∉ m → m[a]? = none
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.coe_top : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A], ↑⊤ = Set.univ
-- Mathlib.Order.Category.Lat
Lat.coe_of : ∀ (X : Type u) [inst : Lattice X], ↑(Lat.of X) = X
-- Mathlib.Order.CompleteBooleanAlgebra
/-- A `biSup` version of `iSup_symmDiff_iSup_le`.  -/
biSup_symmDiff_biSup_le : ∀ {α : Type u} {ι : Sort w} [inst : CompleteBooleanAlgebra α] {p : ι → Prop} {f g : (i : ι) → p i → α},
  symmDiff (⨆ i, ⨆ (h : p i), f i h) (⨆ i, ⨆ (h : p i), g i h) ≤ ⨆ i, ⨆ (h : p i), symmDiff (f i h) (g i h)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.hom_ext : ∀ {X Y : PartOrdEmb} {f g : X ⟶ Y}, PartOrdEmb.Hom.hom f = PartOrdEmb.Hom.hom g → f = g
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Function.Surjective.tsum_eq_tsum_of_hasSum_iff_hasSum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [T2Space α]
  {α' : Type u_4} [inst_3 : AddCommMonoid α'] [inst_4 : TopologicalSpace α'] {e : α' → α},
  Function.Surjective e →
    e 0 = 0 →
      ∀ {f : β → α} {g : γ → α'}, (∀ {a : α'}, HasSum f (e a) ↔ HasSum g a) → ∑' (b : β), f b = e (∑' (c : γ), g c)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_uliftYoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {S : C}
  {ι : Type u_2} [inst_1 : Small.{max w v, u_2} ι] {X : ι → C} (f : (i : ι) → X i ⟶ S),
  CategoryTheory.Sieve.ofArrows X f ∈ J S ↔
    CategoryTheory.Presheaf.IsLocallySurjective J
      (CategoryTheory.Limits.Sigma.desc fun i => CategoryTheory.uliftYoneda.{w, v, u}.map (f i))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, k ∉ t₂ → (t₁ ∩ t₂).getKey! k = default
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
Std.Iterators.Types.TakeWhile.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)}
  (inner inner_1 : Std.IterM m β), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.IsOrtho.orthogonalProjectionOnto_comp_subtypeL`.

---

The projection into `U` from an orthogonal submodule `V` is the zero map.  -/
Submodule.IsOrtho.orthogonalProjection_comp_subtypeL : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} [inst_3 : U.HasOrthogonalProjection], U ⟂ V → U.orthogonalProjectionOnto ∘SL V.subtypeL = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.match_1.splitter : (motive : ℕ → Sort u_1) → (curr : ℕ) → (Unit → motive 0) → ((curr : ℕ) → motive curr.succ) → motive curr
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure_preimage : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (f : G ≃ₜ G),
  (∀ ⦃K : TopologicalSpace.Compacts G⦄, μ (TopologicalSpace.Compacts.map ⇑f ⋯ K) = μ K) →
    ∀ (A : Set G), μ.outerMeasure (⇑f ⁻¹' A) = μ.outerMeasure A
-- Lean.Elab.Tactic.RCases
/-- This introduces the list of patterns `pats`. It has the same arguments as `rcasesCore`, plus:
* `ty?`: the nearest enclosing type ascription on the current pattern
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.rintroContinue : {α : Type} →
  Lean.MVarId →
    Lean.Meta.FVarSubst →
      Array Lean.FVarId →
        Lean.Syntax →
          Lean.TSyntaxArray `rintroPat →
            Option Lean.Term →
              α →
                (Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α) →
                  Lean.Elab.TermElabM α
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
/-- The constant `C` provided by the definition of `LiouvilleWith` can be made positive.
We also add `1 ≤ n` to the list of assumptions about the denominator. While it is equivalent to
the original statement, the case `n = 0` breaks many arguments.  -/
LiouvilleWith.exists_pos : ∀ {p x : ℝ},
  LiouvilleWith p x →
    ∃ C, ∃ (_ : 0 < C), ∃ᶠ (n : ℕ) in Filter.atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- `coe_fn` as an `AddMonoidHom`.  -/
LieDerivation.coeFnAddMonoidHom : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [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] → LieDerivation R L M →+ L → M
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- Given a measure space with an action of a
finite additive group `G`, the measure of any `G`-invariant set is determined by the measure of
its intersection with a fundamental domain for the action of `G`.  -/
MeasureTheory.IsAddFundamentalDomain.measure_eq_card_smul_of_vadd_ae_eq_self : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G]
  [Finite G],
  MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (t : Set α), (∀ (g : G), g +ᵥ t =ᵐ[μ] t) → μ t = Nat.card G • μ (t ∩ s)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousWithinAt.const_cpow : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ} {s : Set α} {a : α} {b : ℂ},
  ContinuousWithinAt f s a → b ≠ 0 ∨ f a ≠ 0 → ContinuousWithinAt (fun x => b ^ f x) s a
-- Mathlib.Data.Set.Prod
Set.preimage_prod_map_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (s : Set β) (t : Set δ),
  Prod.map f g ⁻¹' s ×ˢ t = (f ⁻¹' s) ×ˢ (g ⁻¹' t)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stepAux.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (x : σ)
  (x_1 : (k : K) → List (Γ k)) (k : K) (f : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stepAux (Turing.TM2.Stmt.peek k f q) x x_1 = Turing.TM2.stepAux q (f x (x_1 k).head?) x_1
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_eq_one_iff : ∀ {o : Ordinal.{u_1}}, o.cof = 1 ↔ o ∈ Set.range Order.succ
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Mon.sharesVar.eq_def : ∀ (x x_1 : Lean.Grind.CommRing.Mon),
  x.sharesVar x_1 =
    match x, x_1 with
    | Lean.Grind.CommRing.Mon.unit, x => false
    | x, Lean.Grind.CommRing.Mon.unit => false
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ =>
      match compare pw₁.x pw₂.x with
      | Ordering.eq => true
      | Ordering.lt => m₁.sharesVar (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
      | Ordering.gt => (Lean.Grind.CommRing.Mon.mult pw₁ m₁).sharesVar m₂
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : C) (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app._auto_1),
  (CategoryTheory.Functor.commShiftIso (CategoryTheory.opOp C) n).hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).hom.app (Opposite.op X)).op
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app (Opposite.op (Opposite.op X)))
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Complex.hasStrictFDerivAt_cpow : ∀ {p : ℂ × ℂ},
  p.1 ∈ Complex.slitPlane →
    HasStrictFDerivAt (fun x => x.1 ^ x.2)
      ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ +
        (p.1 ^ p.2 * Complex.log p.1) • ContinuousLinearMap.snd ℂ ℂ ℂ)
      p
-- Mathlib.RingTheory.TensorProduct.Maps
/-- If multiplication by elements of S can switch between the two factors of `S ⊗[R] S`,
then `lmul''` is an isomorphism.  -/
Algebra.TensorProduct.lmulEquiv : (R : Type uR) →
  (S : Type uS) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] → [TensorProduct.CompatibleSMul R S S S] → TensorProduct R S S ≃ₐ[S] S
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Being cofiltered is preserved by equivalence of categories.  -/
CategoryTheory.IsCofiltered.of_equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (h : C ≌ D), CategoryTheory.IsCofiltered D
-- Init.Data.List.TakeDrop
List.takeWhile_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool},
  List.takeWhile p (List.replicate n a) = if p a = true then List.replicate n a else []
-- Lean.Parser.Term
Lean.Parser.Term.nomatch.formatter : Lean.PrettyPrinter.Formatter