mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.isIso_arrow_iff_eq_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y : C} (P : CategoryTheory.Subobject Y),
  CategoryTheory.IsIso P.arrow ↔ P = ⊤
-- Std.Data.TreeSet.Iterator
Std.TreeSet.toList_iter : ∀ {α : Type u_1} {cmp : α → α → Ordering} (m : Std.TreeSet α cmp), m.iter.toList = m.toList
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.base_change : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] (B : Type u_3)
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallyUnramified R A],
  Algebra.FormallyUnramified B (TensorProduct R B A)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.inv_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G)
  [inst_2 : CategoryTheory.IsIso α],
  CategoryTheory.inv (CategoryTheory.NatTrans.op α) = CategoryTheory.NatTrans.op (CategoryTheory.inv α)
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Algebra.TensorProduct.algEquivIncludeRange_toAlgHom : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring T] [inst_4 : Algebra R T],
  ↑(Algebra.TensorProduct.algEquivIncludeRange R S T) =
    Algebra.TensorProduct.map Algebra.TensorProduct.includeLeft.rangeRestrict
      Algebra.TensorProduct.includeRight.rangeRestrict
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.of_coeff_apply : ∀ {Γ : Type u_1} [inst : PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst_1 : CommRing R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddCommGroup W] [inst_5 : Module R W] (f : Γ → V →ₗ[R] W)
  (hf : ∀ (x : V), (Function.support fun x_1 => (f x_1) x).IsPWO) (x : V),
  (HVertexOperator.of_coeff f hf) x = (HahnModule.of R) { coeff := fun g => (f g) x, isPWO_support' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.congrHom.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X ⟶ Z} {g₁ g₂ : Y ⟶ Z} (h₁ : f₁ = f₂)
  (h₂ : g₁ = g₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ g₁] [inst_2 : CategoryTheory.Limits.HasPullback f₂ g₂],
  CategoryTheory.Limits.pullback.congrHom h₁ h₂ = CategoryTheory.Limits.pullback.congrHom h₁ h₂
-- Batteries.Data.List.Basic
List.rotate'.eq_1 : ∀ {α : Type u_1} (x : ℕ), [].rotate' x = []
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Define a pass that tries replacing one terminal tactic with another.

`newTacticName` is a human-readable name for the tactic, for example "linarith".
This can be used to group messages together, so that `ring`, `ring_nf`, `ring1`, ...
all produce the same message.

`oldTacticKind` is the `SyntaxNodeKind` for the tactic's main parser,
for example `Mathlib.Tactic.linarith`.

`newTactic stx goal` selects the new tactic to try, which may depend on the old tactic invocation
in `stx` and the current `goal`.
 -/
Mathlib.TacticAnalysis.terminalReplacement : String →
  String →
    Lean.SyntaxNodeKind →
      (Lean.Elab.ContextInfo →
          Lean.Elab.TacticInfo → Lean.Syntax → Lean.Elab.Command.CommandElabM (Lean.TSyntax `tactic)) →
        optParam Bool true →
          optParam Bool false → optParam Bool false → optParam Float 1 → Mathlib.TacticAnalysis.Config
-- Init.Data.Option.Lemmas
Option.lt.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (val : β), Option.lt r none (some val) = True
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim_inv_app : ∀ (α : Type w₂) {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C] (X : α → C),
  (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim α).inv.app X =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit (CategoryTheory.Discrete.functor X))
-- Mathlib.CategoryTheory.Presentable.Directed
/-- [Stacks Tag 0032](https://stacks.math.columbia.edu/tag/0032) -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed : ∀ (J : Type w) [inst : CategoryTheory.SmallCategory J] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ], ∃ α x, ∃ (_ : CategoryTheory.IsCardinalFiltered α κ), ∃ F, F.Final
-- Init.Data.UInt.Lemmas
UInt8.toFin_ofBitVec : ∀ {b : BitVec 8}, { toBitVec := b }.toFin = b.toFin
-- Init.Data.SInt.Float
/-- Truncates a floating-point number to the nearest word-sized signed integer, rounding towards zero.

If the `Float` is larger than the maximum value for `ISize` (including `Inf`), returns the maximum
value of `ISize` (i.e. `ISize.maxValue`). If it is smaller than the minimum value for `ISize`
(including `-Inf`), returns the minimum value of `ISize` (i.e. `ISize.minValue`). If it is `NaN`,
returns `0`.

This function does not reduce in the kernel.
 -/
Float.toISize : Float → ISize
-- Std.Http.Data.Chunk
Std.Http.Chunk.instBEqExtensionValue.beq : Std.Http.Chunk.ExtensionValue → Std.Http.Chunk.ExtensionValue → Bool
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.State.mk.inj : ∀ {pendingProducer : Option Std.Http.Body.Channel.Producer✝} {pendingConsumer : Option Std.Http.Body.Channel.Consumer✝}
  {interestWaiter : Option (Std.Async.Waiter Bool)} {closed : Bool} {knownSize : Option Std.Http.Body.Length}
  {pendingIncompleteChunk : Option Std.Http.Chunk} {pendingProducer_1 : Option Std.Http.Body.Channel.Producer✝}
  {pendingConsumer_1 : Option Std.Http.Body.Channel.Consumer✝} {interestWaiter_1 : Option (Std.Async.Waiter Bool)}
  {closed_1 : Bool} {knownSize_1 : Option Std.Http.Body.Length} {pendingIncompleteChunk_1 : Option Std.Http.Chunk},
  { pendingProducer := pendingProducer, pendingConsumer := pendingConsumer, interestWaiter := interestWaiter,
        closed := closed, knownSize := knownSize, pendingIncompleteChunk := pendingIncompleteChunk } =
      { pendingProducer := pendingProducer_1, pendingConsumer := pendingConsumer_1, interestWaiter := interestWaiter_1,
        closed := closed_1, knownSize := knownSize_1, pendingIncompleteChunk := pendingIncompleteChunk_1 } →
    pendingProducer = pendingProducer_1 ∧
      pendingConsumer = pendingConsumer_1 ∧
        interestWaiter = interestWaiter_1 ∧
          closed = closed_1 ∧ knownSize = knownSize_1 ∧ pendingIncompleteChunk = pendingIncompleteChunk_1
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.val_run_step_toIterM_iter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {z : Std.DTreeMap.Internal.RxoIterator α β},
  ↑{ internalState := z }.toIterM.step.run.inflate = z.step
-- Mathlib.GroupTheory.CommutingProbability
DihedralGroup.commProb_nil : commProb (DihedralGroup.Product []) = 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
eq_zero_of_add_nonpos_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : PartialOrder α] [AddRightMono α] {a b : α},
  0 ≤ a → 0 ≤ b → a + b ≤ 0 → b = 0
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_list_const_inv : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
  {inv : β → Pred} {epost : EPred},
  (∀ (x : α) (hx : x ∈ xs) (b : β),
      ⦃ inv b ⦄ f x hx b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv b'
        | ForInStep.done b' => inv b';
        epost ⦄) →
    ⦃ inv init ⦄ forIn' xs init f ⦃ inv; epost ⦄
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.drop.match_1.eq_1 : ∀ (motive : Substring.Raw → ℕ → Sort u_1) (s : String) (b e : String.Pos.Raw) (n : ℕ)
  (h_1 :
    (ss : Substring.Raw) →
      (s : String) →
        (b e : String.Pos.Raw) →
          ss = { str := s, startPos := b, stopPos := e } →
            (n : ℕ) → motive { str := s, startPos := b, stopPos := e } n),
  (match { str := s, startPos := b, stopPos := e }, n with
    | ss@h:{ str := s, startPos := b, stopPos := e }, n => h_1 ss s b e h n) =
    h_1 { str := s, startPos := b, stopPos := e } s b e ⋯ n
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.idealOfSet_ofIdeal_isClosed : ∀ {X : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [CompactSpace X] [T2Space X]
  {I : Ideal C(X, 𝕜)}, IsClosed ↑I → ContinuousMap.idealOfSet 𝕜 (ContinuousMap.setOfIdeal I) = I
-- Mathlib.Algebra.Group.TransferInstance
Equiv.sub_def : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Sub β] (x y : α), x - y = e.symm (e x - e y)
-- Init.Data.Array.MinMax
_private.Init.Data.Array.MinMax.0.Array.min.eq_1 : ∀ {α : Type u_1} [inst : Min α] (arr : Array α) (h : arr ≠ #[]), arr.min h = Array.foldl min arr[0] arr 1
-- ProofWidgets.Cancellable
/-- The status of a running cancellable request.  -/
ProofWidgets.CheckRequestResponse : Type
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- Continuous functions vanishing at infinity taking values in a complete space form a
complete space.  -/
ZeroAtInftyContinuousMap.instCompleteSpace : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
  [CompleteSpace β], CompleteSpace (ZeroAtInftyContinuousMap α β)
-- Batteries.Control.AlternativeMonad
LawfulAlternative.mk : ∀ {m : Type u_1 → Type u_2} [inst : Alternative m] [toLawfulApplicative : LawfulApplicative m],
  (∀ {α β : Type u_1} (f : α → β), f <$> failure = failure) →
    (∀ {α β : Type u_1} (x : m α), failure <*> x = failure) →
      (∀ {α : Type u_1} (x : m α), (x <|> failure) = x) →
        (∀ {α : Type u_1} (y : m α), (failure <|> y) = y) →
          (∀ {α : Type u_1} (x y z : m α), (x <|> y <|> z) = ((x <|> y) <|> z)) →
            (∀ {α β : Type u_1} (x y : m α) (f : α → β), f <$> (x <|> y) = (f <$> x <|> f <$> y)) → LawfulAlternative m
-- Mathlib.Algebra.Group.Basic
eq_div_iff_mul_eq'' : ∀ {G : Type u_3} [inst : CommGroup G] {a b c : G}, a = b / c ↔ c * a = b
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.models_iff_not_satisfiable : ∀ {L : FirstOrder.Language} {T : L.Theory} (φ : L.Sentence),
  T ⊨ᵇ φ ↔ ¬(T ∪ {FirstOrder.Language.Formula.not φ}).IsSatisfiable
-- Std.Time.Notation.Spec
_private.Std.Time.Notation.Spec.0.Std.Time.convertFraction : Std.Time.Fraction → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Order.Defs.Unbundled
ne_of_irrefl' : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Irrefl r] {x y : α}, r x y → y ≠ x
-- Mathlib.Data.Real.Sign
Real.sign_intCast : ∀ (z : ℤ), (↑z).sign = ↑z.sign
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.discr.eq_1 : ∀ {R : Type u_3} {N : Type u_5} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : Invertible 2] [inst_4 : AddCommGroup N] [inst_5 : Module R N] (b : Module.Basis n R N)
  (Q : QuadraticForm R N), QuadraticForm.discr b Q = (QuadraticForm.toMatrix b Q).det
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurable_infDist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α},
  Measurable fun x => Metric.infDist x s
-- Mathlib.Computability.Primrec.Basic
Primrec.not : Primrec not
-- Lean.Meta.WHNF
/-- Consumes unused `let`s/`have`s.
If `consumeNondep` is false, then `have`s are not consumed.

Auxiliary function for `whnfCore`, `isDefEqQuick`, and `Simp.reduceStep`,
to implement the `zetaUnused` option.
In the case of `isDefEqQuick`, it is also used when `zeta` is set.
 -/
Lean.Meta.consumeUnusedLet : Lean.Expr → optParam Bool false → Lean.Expr
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_fun_mul' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a b : E → 𝔸},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 a s x →
      DifferentiableWithinAt 𝕜 b s x →
        fderivWithin 𝕜 (fun y => a y * b y) s x =
          a x • fderivWithin 𝕜 b s x + MulOpposite.op (b x) • fderivWithin 𝕜 a s x
-- Mathlib.Computability.Encoding
_private.Mathlib.Computability.Encoding.0.Computability.decodePosNum.match_1.eq_1 : ∀ (motive : List Bool → Sort u_1) (l : List Bool) (h_1 : (l : List Bool) → motive (false :: l))
  (h_2 : (l : List Bool) → motive (true :: l)) (h_3 : (x : List Bool) → motive x),
  (match false :: l with
    | false :: l => h_1 l
    | true :: l => h_2 l
    | x => h_3 x) =
    h_1 l
-- Init.Data.Fin.Lemmas
Fin.succ_pos : ∀ {n : ℕ} (a : Fin n), 0 < a.succ
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.ae_lt_top_of_comp_ne_top : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ} {s : Set γ} (a : α),
  ((η.comp κ) a) s ≠ ⊤ → ∀ᵐ (b : β) ∂κ a, (η b) s < ⊤
-- Std.Data.Internal.List.Associative
Option.map.eq_def : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : Option α),
  Option.map f x =
    match x with
    | some x => some (f x)
    | none => none
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_inj : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o a b : Ordinal.{u}},
  Order.IsNormal f → (Ordinal.veblenWith f o a = Ordinal.veblenWith f o b ↔ a = b)
-- Mathlib.Data.Num.Lemmas
PosNum.size_to_nat : ∀ (n : PosNum), ↑n.size = (↑n).size
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₁_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] {υ : Type u_6} (f : τ → MvPolynomial υ R)
  (g : σ → τ) (φ : MvPolynomial σ R),
  (MvPolynomial.bind₁ f) ((MvPolynomial.rename g) φ) = (MvPolynomial.bind₁ (f ∘ g)) φ
-- Lean.Elab.SyntheticMVars
/-- Similar to `synthesizeInstMVarCore`, but makes sure that `instMVar` local context and instances
are used. It also logs any error message produced.  -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizePendingInstMVar : Lean.MVarId → optParam (Option Lean.MessageData) none → Lean.Elab.TermElabM Bool
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem_toArray_rio : ∀ {n i : ℕ} (_h : i < (*...n).toArray.size), (*...n).toArray[i] = i
-- Mathlib.Data.Nat.Bits
Nat.boddDiv2_eq : ∀ (n : ℕ), n.boddDiv2 = (n.bodd, n.div2)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.homEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x y : CategoryTheory.ComposableArrows C 0},
  CategoryTheory.nerve.homEquiv =
    {
      toFun := fun e =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.hom e.edge) (CategoryTheory.eqToHom ⋯)),
      invFun := fun f => SSet.Edge.mk (CategoryTheory.ComposableArrows.mk₁ f) ⋯ ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.toList_insert_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : BEq α] [Std.TransCmp cmp] [Std.LawfulBEqCmp cmp]
  {k : α}, (t.insert k).toList.Perm (if k ∈ t then t.toList else k :: t.toList)
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
ProbabilityTheory.HasIndepIncrements.map' : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : Preorder T] [inst_1 : MeasurableSpace E] {F : Type u_4} {G : Type u_5} [inst_2 : MeasurableSpace G]
  [inst_3 : FunLike F E G] [inst_4 : AddGroup E] [inst_5 : SubtractionMonoid G] [AddMonoidHomClass F E G] {f : F},
  Measurable ⇑f →
    ProbabilityTheory.HasIndepIncrements X P → ProbabilityTheory.HasIndepIncrements (fun t ω => f (X t ω)) P
-- Mathlib.Data.Countable.Basic
instCountableSum : ∀ {α : Type u} {β : Type v} [Countable α] [Countable β], Countable (α ⊕ β)
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instInhabited.eq_1 : ∀ {α : Type u_1} [inst : LE α], LowerSet.instInhabited = { default := ⊤ }
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.comp.injEq : ∀ {C : Type u} {X Y Z : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y) (g : Y.Hom Z)
  (Y_1 : CategoryTheory.FreeMonoidalCategory C) (f_1 : X.Hom Y_1) (g_1 : Y_1.Hom Z),
  (f.comp g = f_1.comp g_1) = (Y = Y_1 ∧ f ≍ f_1 ∧ g ≍ g_1)
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'}
  (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) {Z : C} (h : (data.factorizationData g).Z ⟶ Z),
  CategoryTheory.CategoryStruct.comp (data.factorizationData f).i (CategoryTheory.CategoryStruct.comp (data.mapZ φ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left φ)
      (CategoryTheory.CategoryStruct.comp (data.factorizationData g).i h)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.orthogonalProjectionOnto_orthogonalComplement_singleton_eq_zero`.

---

The orthogonal projection onto `(𝕜 ∙ v)ᗮ` of `v` is zero.  -/
Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (v : E), (𝕜 ∙ v)ᗮ.orthogonalProjectionOnto v = 0
-- Init.Data.Array.Zip
Array.take_zipWith : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {as : Array α} {bs : Array α_1} {i : ℕ},
  (Array.zipWith f as bs).take i = Array.zipWith f (as.take i) (bs.take i)
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHSubOffset : HSub Std.Time.WallTime Std.Time.Day.Offset Std.Time.WallTime
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_one_of_isEmpty : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (A : Matrix n n R)
  [IsEmpty n], Matrix.detp 1 A = 1
-- Init.Data.SInt.IntToBitVec
ISize.le_iff_toBitVec32_sle : ∀ {a b : ISize} (h : System.Platform.numBits = 32), a ≤ b ↔ (a.toBitVec32 h).sle (b.toBitVec32 h) = true
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.lratChecker.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} {inst : DecidableEq α} [inst_1 : DecidableEq α]
  [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] [inst_3 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ]
  [inst_4 : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f f_1 : σ),
  f = f_1 →
    ∀ (prf prf_1 : List (Std.Tactic.BVDecide.LRAT.Action β α)),
      prf = prf_1 →
        Std.Tactic.BVDecide.LRAT.Internal.lratChecker f prf = Std.Tactic.BVDecide.LRAT.Internal.lratChecker f_1 prf_1
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
/-- Map a homogeneous ideal along a graded ring homomorphism. The underlying ideal is
(definitionally) equal to `Ideal.map`.  -/
HomogeneousIdeal.map : {A : Type u_1} →
  {B : Type u_2} →
    {σ : Type u_4} →
      {τ : Type u_5} →
        {ι : Type u_7} →
          [inst : Semiring A] →
            [inst_1 : Semiring B] →
              [inst_2 : SetLike σ A] →
                [inst_3 : SetLike τ B] →
                  [inst_4 : AddSubmonoidClass σ A] →
                    [inst_5 : AddSubmonoidClass τ B] →
                      [inst_6 : DecidableEq ι] →
                        [inst_7 : AddMonoid ι] →
                          {𝒜 : ι → σ} →
                            {ℬ : ι → τ} →
                              [inst_8 : GradedRing 𝒜] →
                                [inst_9 : GradedRing ℬ] → (𝒜 →+*ᵍ ℬ) → HomogeneousIdeal 𝒜 → HomogeneousIdeal ℬ
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.zero_mem : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : SubMulAction R M),
  (↑p).Nonempty → 0 ∈ p
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.Decomposition.inductionOn : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [DirectSum.Decomposition ℳ] {motive : M → Prop},
  motive 0 →
    (∀ {i : ι} (m : ↥(ℳ i)), motive ↑m) → (∀ (m m' : M), motive m → motive m' → motive (m + m')) → ∀ (m : M), motive m
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.card_mul : ∀ (a b : Ordinal.{u_4}), (a * b).card = a.card * b.card
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.smul_addMonoidHom_apply : ∀ {A : Type u_5} {B : Type u_6} {M : Type u_7} [inst : AddMonoid A] [inst_1 : DistribSMul M A] [inst_2 : AddZeroClass B]
  (c : Mᵈᵐᵃ) (f : A →+ B) (a : A), (c • f) a = f (DomMulAct.mk.symm c • a)
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.instCoeSortType : {R : Type u} → [inst : CommRing R] → CoeSort (CommBialgCat R) (Type v)
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellation.mk.sizeOf_spec : sizeOf { } = 1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.mk.injEq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cocone F} (hom : A.pt ⟶ B.pt)
  (w :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι.app j) hom = B.ι.app j)
      CategoryTheory.Limits.CoconeMorphism.w._autoParam)
  (hom_1 : A.pt ⟶ B.pt)
  (w_1 :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι.app j) hom_1 = B.ι.app j)
      CategoryTheory.Limits.CoconeMorphism.w._autoParam),
  ({ hom := hom, w := w } = { hom := hom_1, w := w_1 }) = (hom = hom_1)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp_symm_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) {X X' : F.PartialLeftAdjointSource} {Y : D} (f : X'.obj ⟶ F.obj Y) (g : X ⟶ X')
  {Z : D} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.partialLeftAdjointMap g)
      (CategoryTheory.CategoryStruct.comp (F.partialLeftAdjointHomEquiv.symm f) h) =
    CategoryTheory.CategoryStruct.comp (F.partialLeftAdjointHomEquiv.symm (CategoryTheory.CategoryStruct.comp g.hom f))
      h
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.addLeftStrictMono : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddMonoid N] [inst_2 : LinearOrder N]
  [AddLeftStrictMono N], AddLeftStrictMono (Lex (α →₀ N))
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.symm_trans_source_eq : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e e' : Bundle.Pretrivialization F proj),
  (e.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ
-- Mathlib.Data.Matrix.Mul
Matrix.isLeftRegular_iff_mulVec_injective : ∀ {m : Type u_2} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype m] {A : Matrix m m α},
  IsLeftRegular A ↔ Function.Injective A.mulVec
-- Mathlib.Topology.Partial
/-- Continuity of a partial function  -/
PContinuous : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X →. Y) → Prop