mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Separable
Polynomial.separable_gcd_right : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq (Polynomial F)] {g : Polynomial F} (f : Polynomial F),
  g.Separable → (EuclideanDomain.gcd f g).Separable
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.not_isClosedSubgraph_iff_exists_adj : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β},
  H.IsInducedSubgraph G → (¬H.IsClosedSubgraph G ↔ ∃ x y, G.Adj x y ∧ x ∈ H.vertexSet ∧ y ∉ H.vertexSet)
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.apply_inr_eq_zero_of_mem_span_range_u : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : DecidableEq ι] (j : ι) {x : ↥b.support ⊕ ι → R},
  x ∈ Submodule.span R (Set.range RootPairing.GeckConstruction.u) → x (Sum.inr j) = 0
-- Init.SimpLemmas
iff_self_or : ∀ {a b : Prop}, (a ↔ a ∨ b) ↔ b → a
-- Mathlib.MeasureTheory.PiSystem
/-- A Dynkin system is closed under complementation.  -/
MeasurableSpace.DynkinSystem.has_compl : ∀ {α : Type u_4} (self : MeasurableSpace.DynkinSystem α) {a : Set α}, self.Has a → self.Has aᶜ
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.instVAddCommClassSubtypeMem_1 : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : VAdd α β]
  [inst_2 : VAdd M' β] [VAddCommClass α M' β], VAddCommClass α (↥s) β
-- Init.Grind.Interactive
/-- `try tac` runs `tac` and succeeds even if `tac` failed.  -/
Lean.Parser.Tactic.Grind.grindTry_ : Lean.ParserDescr
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.eq_iff_exists : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {x y : M}, f x = f y ↔ ∃ c, ↑c + x = ↑c + y
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  (∀ (Y : C), Nonempty (Unique (X ⟶ Y))) → (∀ (Y : C), Nonempty (Unique (Y ⟶ X))) → CategoryTheory.Limits.IsZero X
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.minValueSealed : ISize
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_left_inj' : ∀ {w : ℕ} (a b c : BitVec w), (a ^^^ c == c ^^^ b) = (a == b)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative commutes with shifting the function by a constant on the right.  -/
iteratedFDeriv_comp_add_right' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  (n : ℕ) (a : E), (iteratedFDeriv 𝕜 n fun z => f (z + a)) = fun x => iteratedFDeriv 𝕜 n f (x + a)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.equiv_empty_iff_isEmpty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m.WF → (m.Equiv ∅ ↔ m.isEmpty = true)
-- Mathlib.Algebra.Ring.SumsOfSquares
IsSumSq.brecOn : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] {motive : (a : R) → IsSumSq a → Prop} {a : R}
  (t : IsSumSq a), (∀ (a : R) (t : IsSumSq a), IsSumSq.below t → motive a t) → motive a t
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_fun_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x →
    DifferentiableWithinAt 𝕜 f s x →
      derivWithin (fun y => c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x
-- Mathlib.Data.FunLike.Group
FunLike.addMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : SMul ℕ F] [inst_4 : AddMonoid β] [inst_5 : IsZeroApply F α β] [inst_6 : IsAddApply F α β]
  [inst_7 : IsSMulApply ℕ F α β], FunLike.addMonoid = Function.Injective.addMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.prehaar_mem_haarProduct : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G},
  (interior U).Nonempty → MeasureTheory.Measure.haar.prehaar (↑K₀) U ∈ MeasureTheory.Measure.haar.haarProduct ↑K₀
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiableOn_of_locally_differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {s : Set E},
  (∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)) → DifferentiableOn 𝕜 f s
-- Init.Data.Array.Nat
Array.prod_pos_iff_forall_pos_nat : ∀ {xs : Array ℕ}, 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x
-- Lean.Elab.Declaration
Lean.Elab.Command.expandMutualElement : Lean.Macro
-- Init.Data.UInt.Bitwise
UInt32.ofFin_or : ∀ (a b : Fin UInt32.size), UInt32.ofFin (a ||| b) = UInt32.ofFin a ||| UInt32.ofFin b
-- Mathlib.Computability.Ackermann
ack_strictMono_right : ∀ (m : ℕ), StrictMono (ack m)
-- Mathlib.RepresentationTheory.Coinduced
/-- The morphism induced by the adjunction between `res φ` and `coind φ` sending a morphism
`f : res φ B ⟶ A` to the morphism `B ⟶ coind φ A` given by the underlying linear map sending
`b : B.V` to the function sending `h : H` to `f ((B.ρ h) b)`.  -/
Rep.resCoindToHom : {k : Type u} →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            (φ : G →* H) →
              (B : Rep.{max u_1 w, u, w} k H) →
                (A : Rep.{max u_1 w, u, v} k G) → (Rep.res φ B ⟶ A) → (B ⟶ Rep.coind.{u, v, w, max u_1 w} φ A)
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_fin_three_of : ∀ {R : Type u_6} [inst : AddCommMonoid R] (a b c d e f g h i : R), !![a, b, c; d, e, f; g, h, i].trace = a + e + i
-- Mathlib.LinearAlgebra.Dimension.Finite
Module.finite_of_rank_eq_one : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M],
  Module.rank R M = 1 → Module.Finite R M
-- Plausible.Random
/-- `BoundedRandom m α` gives us machinery to generate values of type `α` between certain bounds in
the monad `m`.  -/
Plausible.BoundedRandom : (Type u → Type u_1) → (α : Type u) → [LE α] → Type (max (max 1 u) u_1)
-- Mathlib.Order.Filter.Cofinite
/-- An injective sequence `f : ℕ → ℕ` tends to infinity at infinity.  -/
Function.Injective.nat_tendsto_atTop : ∀ {f : ℕ → ℕ}, Function.Injective f → Filter.Tendsto f Filter.atTop Filter.atTop
-- Mathlib.Topology.GDelta.Basic
/-- A set is nowhere dense if it is nowhere dense in some subspace.  -/
IsNowhereDense.image_val : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Set X} {s : Set ↑Y},
  IsNowhereDense s → IsNowhereDense (Subtype.val '' s)
-- Mathlib.Algebra.Ring.Commute
Commute.mul_self_sub_mul_self_eq' : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {a b : R}, Commute a b → a * a - b * b = (a - b) * (a + b)
-- Mathlib.Topology.Order.Basic
isOpen_gt' : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] (a : α), IsOpen {b | b < a}
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIso_hom_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {s t : CategoryTheory.Bicategory.LeftLift f g} (P : s.IsKan) (Q : t.IsKan),
  CategoryTheory.StructuredArrow.Hom.right (P.uniqueUpToIso Q).hom = P.desc t
-- Mathlib.Algebra.Group.AddChar
AddChar.ext : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (f g : AddChar A M),
  (∀ (x : A), f x = g x) → f = g
-- Mathlib.Topology.Algebra.Monoid.Defs
SeparatelyContinuousAdd.continuous_add_const : ∀ {M : Type u_1} {inst : TopologicalSpace M} {inst_1 : Add M} [self : SeparatelyContinuousAdd M] {a : M},
  Continuous fun x => x + a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.not_equiv_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P 2 = 0 → Q 2 ≠ 0 → ¬P ≈ Q
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.max?.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 : (c : RBTree.RBColor) → (l : RBTree.RBNode α) → (v : α) → motive (RBTree.RBNode.node c l v RBTree.RBNode.nil))
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (match RBTree.RBNode.node c l v RBTree.RBNode.nil with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c l v RBTree.RBNode.nil => h_2 c l v
    | RBTree.RBNode.node c l v r => h_3 c l v r) =
    h_2 c l v
-- Plausible.Testable
Plausible.instToExprConfiguration : Lean.ToExpr Plausible.Configuration
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_Icc : ∀ {α : Type u_1} [inst : Preorder α] [LocallyFiniteOrder α] (a b : α), (Set.Icc a b).Finite
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_fun_add : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.variance (fun ω => X ω + Y ω) μ =
        ProbabilityTheory.variance X μ + 2 * ProbabilityTheory.covariance X Y μ + ProbabilityTheory.variance Y μ
-- Init.Data.Repr
/-- Returns the decimal representation of a natural number as a list of digit characters in the given
base. If the base is greater than `16` then `'*'` is returned for digits greater than `0xf`.

Examples:
* `Nat.toDigits 10 0xff = ['2', '5', '5']`
* `Nat.toDigits 8 0xc = ['1', '4']`
* `Nat.toDigits 16 0xcafe = ['c', 'a', 'f', 'e']`
* `Nat.toDigits 80 200 = ['2', '*']`
 -/
Nat.toDigits : ℕ → ℕ → List Char
-- Mathlib.Analysis.Normed.Affine.AddTorsor
AddMonoidHom.ofMapMidpoint.congr_simp : ∀ (R : Type u_1) (R' : Type u_2) {E : Type u_3} {F : Type u_4} [inst : Ring R] [inst_1 : Invertible 2]
  [inst_2 : AddCommGroup E] [inst_3 : Module R E] [inst_4 : Ring R'] [inst_5 : Invertible 2] [inst_6 : AddCommGroup F]
  [inst_7 : Module R' F] (f f_1 : E → F) (e_f : f = f_1) (h0 : f 0 = 0)
  (hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)),
  AddMonoidHom.ofMapMidpoint R R' f h0 hm = AddMonoidHom.ofMapMidpoint R R' f_1 ⋯ ⋯
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.comap_comap : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] [inst_2 : NonAssocRing T]
  (s : Subring T) (g : S →+* T) (f : R →+* S), Subring.comap f (Subring.comap g s) = Subring.comap (g.comp f) s
-- Mathlib.Tactic.Linter.AuxLemma
/-- The `auxLemma` linter emits a warning on any explicit reference to an auto-generated
auxiliary declaration (such as `_proof_1`, `match_1`, or `_sizeOf_1`).

These names are internal to the Lean elaborator and are not stable across refactors.  -/
_private.Mathlib.Tactic.Linter.AuxLemma.0.Mathlib.Linter.AuxLemma.auxLemmaLinter : Lean.Linter
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {f : α → β → Bool} {k : α},
  (Std.ExtHashMap.filter f m).getKey! k = ((m.getKey? k).pfilter fun x_2 h' => f x_2 m[x_2]).get!
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
isCompactOperator_id_iff_locallyCompactSpace : ∀ {E : Type u_1} [inst : AddGroup E] [inst_1 : TopologicalSpace E] [IsTopologicalAddGroup E],
  IsCompactOperator id ↔ LocallyCompactSpace E
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUInfo.mk.injEq : ∀ (model : String) (speed : UInt64) (times : Std.Internal.UV.System.CPUTimes) (model_1 : String) (speed_1 : UInt64)
  (times_1 : Std.Internal.UV.System.CPUTimes),
  ({ model := model, speed := speed, times := times } = { model := model_1, speed := speed_1, times := times_1 }) =
    (model = model_1 ∧ speed = speed_1 ∧ times = times_1)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.mk : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (pt : C) → (F ⟶ (CategoryTheory.Functor.const J).obj pt) → CategoryTheory.Limits.Cocone F
-- Mathlib.Data.Num.ZNum
ZNum.addMonoid : AddMonoid ZNum
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.submodule_comap_pow_reverse : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (p : Submodule R (CliffordAlgebra Q)) (n : ℕ),
  Submodule.comap CliffordAlgebra.reverse (p ^ n) = Submodule.comap CliffordAlgebra.reverse p ^ n
-- Lean.Data.Options
_private.Lean.Data.Options.0.Lean.Options.mk.injEq : ∀ (map : Lean.NameMap Lean.DataValue) (hasTrace : Bool) (map_1 : Lean.NameMap Lean.DataValue) (hasTrace_1 : Bool),
  ({ map := map, hasTrace := hasTrace } = { map := map_1, hasTrace := hasTrace_1 }) =
    (map = map_1 ∧ hasTrace = hasTrace_1)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
WeakBilin.eval_continuous : ∀ {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [inst : TopologicalSpace 𝕜] [inst_1 : CommSemiring 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (y : F), Continuous fun x => (B x) y
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  {ε : 𝕜} [inst_3 : Fintype α] [inst_4 : DecidableRel G.Adj] [Nonempty α] [inst_6 : DecidableEq α],
  G.FarFromTriangleFree ε → 0 < ε → (G.cliqueFinset 3).Nonempty
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.dirac_caratheodory : ∀ {α : Type u_1} (a : α), (MeasureTheory.OuterMeasure.dirac a).caratheodory = ⊤
-- Mathlib.Data.TypeVec
TypeVec.appendFun_id_id : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {β : Type u_1}, (TypeVec.id ::: id) = TypeVec.id
-- Mathlib.Topology.Instances.NNReal.Lemmas
HasSum.toNNReal : ∀ {α : Type u_2} {L : SummationFilter α} {f : α → ℝ} {y : ℝ},
  (∀ (n : α), 0 ≤ f n) → HasSum f y L → HasSum (fun x => (f x).toNNReal) y.toNNReal L
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
_private.Mathlib.AlgebraicGeometry.Morphisms.Flat.0.CategoryTheory.Pairwise.diagramMap.match_1.eq_1 : ∀ {ι : Type u_1} (motive : (x x_1 : CategoryTheory.Pairwise ι) → (x ⟶ x_1) → Sort u_2) (i : ι)
  (h_1 :
    (i : ι) →
      motive (CategoryTheory.Pairwise.single i) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.id_single i))
  (h_2 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.pair i j)
        (CategoryTheory.Pairwise.Hom.id_pair i j))
  (h_3 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.left i j))
  (h_4 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single j)
        (CategoryTheory.Pairwise.Hom.right i j)),
  (match CategoryTheory.Pairwise.single i, CategoryTheory.Pairwise.single i,
      CategoryTheory.Pairwise.Hom.id_single i with
    | .(CategoryTheory.Pairwise.single i), .(CategoryTheory.Pairwise.single i),
      CategoryTheory.Pairwise.Hom.id_single i => h_1 i
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.pair i j),
      CategoryTheory.Pairwise.Hom.id_pair i j => h_2 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single i), CategoryTheory.Pairwise.Hom.left i j =>
      h_3 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single j), CategoryTheory.Pairwise.Hom.right i j =>
      h_4 i j) =
    h_1 i
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.instEquivLike : {R : Type u_2} →
  {M₁ : Type u_5} →
    {M₂ : Type u_6} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] →
                      {Q₁ : QuadraticMap R M₁ N} → {Q₂ : QuadraticMap R M₂ N} → EquivLike (Q₁.IsometryEquiv Q₂) M₁ M₂
-- Mathlib.Data.Set.Operations
/-- Any map `f : ι → α` factors through a map `rangeFactorization f : ι → range f`.  -/
Set.rangeFactorization : {α : Type u} → {ι : Sort u_1} → (f : ι → α) → ι → ↑(Set.range f)
-- Mathlib.Data.List.Basic
List.getLast?_eq_getLast_of_ne_nil : ∀ {α : Type u} {l : List α} (h : l ≠ []), l.getLast? = some (l.getLast h)
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
QuadraticMap.Nondegenerate.mk : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P},
  Q.radical = ⊥ → Module.rank R ↥(LinearMap.ker Q.polarBilin) ≤ 1 → QuadraticMap.Nondegenerate
-- Init.Data.SInt.Lemmas
ISize.mul_add : ∀ {a b c : ISize}, a * (b + c) = a * b + a * c
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckAddGroup.instNeg : {M : Type u_1} → [inst : AddCommMonoid M] → Neg (Algebra.GrothendieckAddGroup M)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
MeasureTheory.SignedMeasure.zero_mem_measureOfNegatives : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α}, 0 ∈ s.measureOfNegatives
-- Batteries.Tactic.Lint.Frontend
/-- `medium`: only print failing checks, print confirmation on success.  -/
Batteries.Tactic.Lint.LintVerbosity.medium : Batteries.Tactic.Lint.LintVerbosity
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.comp_apply : ∀ {X Y T : AddGrpCat} (f : X ⟶ Y) (g : Y ⟶ T) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceMul : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.Ideal.Over
/-- If there is an injective map `R/p → S/P` such that the following diagram commutes:
```
R   → S
↓     ↓
R/p → S/P
```
then `P` lies over `p`.
 -/
Ideal.comap_eq_of_scalar_tower_quotient : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {p : Ideal R} {P : Ideal S}
  [inst_2 : Algebra R S] [inst_3 : Algebra (R ⧸ p) (S ⧸ P)] [IsScalarTower R (R ⧸ p) (S ⧸ P)],
  Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P)) → Ideal.comap (algebraMap R S) P = p
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.id_apply : ∀ {M : Type u_2} {X : Type u_5} [inst : SMul M X] (x : X), (MulActionHom.id M) x = x
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.deterministic.hcongr_6 : ∀ (α α' : Type u_1),
  α = α' →
    ∀ (β β' : Type u_2),
      β = β' →
        ∀ (mα : MeasurableSpace α) (mα' : MeasurableSpace α'),
          mα ≍ mα' →
            ∀ (mβ : MeasurableSpace β) (mβ' : MeasurableSpace β'),
              mβ ≍ mβ' →
                ∀ (f : α → β) (f' : α' → β'),
                  f ≍ f' →
                    ∀ (hf : Measurable f) (hf' : Measurable f'),
                      hf ≍ hf' →
                        ProbabilityTheory.Kernel.deterministic f hf ≍ ProbabilityTheory.Kernel.deterministic f' hf'
-- Std.Data.DHashMap.Raw
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.
 -/
Std.DHashMap.Raw.Const.get? : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → (Std.DHashMap.Raw α fun x => β) → α → Option β
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : CommSemiring R] {f : MvPowerSeries σ R},
  IsNilpotent (MvPowerSeries.constantCoeff f) → IsTopologicallyNilpotent f
-- Mathlib.Data.ENNReal.Basic
Set.OrdConnected.image_coe_nnreal_ennreal : ∀ {t : Set NNReal}, t.OrdConnected → (ENNReal.ofNNReal '' t).OrdConnected
-- Mathlib.Order.GaloisConnection.Defs
/-- A constructor for a Galois coinsertion with the trivial `choice` function.  -/
GaloisCoinsertion.monotoneIntro : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {u : α → β} →
          {l : β → α} →
            Monotone u → Monotone l → (∀ (a : α), l (u a) ≤ a) → (∀ (b : β), u (l b) = b) → GaloisCoinsertion l u
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.toArray_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.toArray = t₂.toArray
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.fold_eq_foldl_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α} {δ : Type v},
  m.WF → ∀ {f : δ → α → δ} {init : δ}, Std.HashSet.Raw.fold f init m = List.foldl f init m.toList
-- Std.Http.Data.Status
/-- 425 Too Early
 -/
Std.Http.Status.tooEarly : Std.Http.Status
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.toContinuousAffineMap_toAffineMap : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), ↑e.toContinuousAffineMap = ↑↑e
-- Mathlib.Algebra.Homology.Square
/-- A commutative square in a preadditive category is a pullback square iff
the corresponding diagram `0 ⟶ X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0` makes `X₁` a kernel.  -/
CategoryTheory.Square.isPullbackEquivIsLimitKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (sq : CategoryTheory.Square C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct sq.X₂ sq.X₃] →
          sq.IsPullback ≃ CategoryTheory.Limits.IsLimit sq.kernelFork
-- Init.Notation
/-- Subtraction of precedences. This is normally used only for offsetting, e.g. `max - 1`.  -/
Lean.Parser.Syntax.subPrec : Lean.TrailingParserDescr
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the largest element of the tree set, returning `none` if the set is empty.
 -/
Std.ExtTreeSet.max? : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → Option α
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorphOn.isDiscrete_of_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsLocalHomeomorphOn f s → IsDiscrete (f '' s) → IsDiscrete s
-- Mathlib.Data.Nat.Digits.Lemmas
_private.Mathlib.Data.Nat.Digits.Lemmas.0.List.alternatingSum.match_1.eq_3 : ∀ {G : Type u_1} (motive : List G → Sort u_2) (g h : G) (t : List G) (h_1 : Unit → motive [])
  (h_2 : (g : G) → motive [g]) (h_3 : (g h : G) → (t : List G) → motive (g :: h :: t)),
  (match g :: h :: t with
    | [] => h_1 ()
    | [g] => h_2 g
    | g :: h :: t => h_3 g h t) =
    h_3 g h t
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- A matrix `M : Matrix n n R` is positive semidefinite if it is Hermitian and `xᴴ * M * x` is
nonnegative for all `x` of finite support.  -/
Matrix.PosSemidef : {n : Type u_2} → {R : Type u_3} → [inst : Ring R] → [PartialOrder R] → [StarRing R] → Matrix n n R → Prop