mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.smulZeroClass' : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {S : Type u_3} →
            [inst_3 : SMul S R] →
              [inst_4 : SMulZeroClass S M] → [IsScalarTower S R M] → (P : Submodule R M) → SMulZeroClass S (M ⧸ P)
-- Mathlib.Data.Matrix.Reflection
/-- `Matrix.mulVec` with better defeq for `Fin`  -/
Matrix.mulVecᵣ : {l m : ℕ} → {α : Type u_1} → [Mul α] → [Add α] → [Zero α] → Matrix (Fin l) (Fin m) α → (Fin m → α) → Fin l → α
-- Mathlib.Order.PFilter
/-- The smallest filter containing a given element.  -/
Order.PFilter.principal : {P : Type u_1} → [inst : Preorder P] → P → Order.PFilter P
-- Lean.Environment
/-- If true, IR is loaded transitively.  -/
_private.Lean.Environment.0.Lean.ImportedModule.needsIRTrans : Lean.ImportedModule✝ → Bool
-- Mathlib.Data.Set.Basic
Set.mem_of_mem_of_subset : ∀ {α : Type u} {x : α} {s t : Set α}, x ∈ s → s ⊆ t → x ∈ t
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.toSubmonoid_injective : ∀ {M : Type u_1} [inst : MulOneClass M], Function.Injective SaturatedSubmonoid.toSubmonoid
-- Mathlib.Order.Interval.Set.Disjoint
Set.Iio_disjoint_Ioi_of_not_lt : ∀ {α : Type v} [inst : Preorder α] {a b : α}, ¬b < a → Disjoint (Set.Iio a) (Set.Ioi b)
-- Mathlib.Topology.Constructions
continuous_quot_mk : ∀ {X : Type u} [inst : TopologicalSpace X] {r : X → X → Prop}, Continuous (Quot.mk r)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.instIsMulCommutative_closure : ∀ {S : Type u_1} {R : Type u_2} [inst : NonUnitalSemiring R] [inst_1 : SetLike S R] [inst_2 : MulMemClass S R] (s : S)
  [IsMulCommutative ↥s], IsMulCommutative ↥(NonUnitalSubsemiring.closure ↑s)
-- Init.Data.List.Basic
List.set.eq_3 : ∀ {α : Type u_1} (x : ℕ) (x_1 : α), [].set x x_1 = []
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsTrivialBlock.image : ∀ {M : Type u_3} {α : Type u_4} {N : Type u_5} {β : Type u_6} [inst : AddMonoid M] [inst_1 : AddAction M α]
  [inst_2 : AddMonoid N] [inst_3 : AddAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Surjective ⇑f → ∀ {B : Set α}, AddAction.IsTrivialBlock B → AddAction.IsTrivialBlock (⇑f '' B)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ext : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} {inst : LinearOrder ι} {f : P.RankFunction ι} {i : ι}
  {x y : f.Cell i}, x.s = y.s → x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.one.sizeOf_spec : sizeOf CategoryTheory.Limits.WalkingReflexivePair.one = 1
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.commSemiring : ℕ → Lean.Meta.Sym.Arith.ClassifyResult
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.addEquivCongrRight_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (e : M ≅ N)
  [inst_4 : CategoryTheory.IsAddMonHom e.hom] (X : C)
  (a : ↑((CategoryTheory.yonedaAddMon.obj { X := M, addMon := inst_2 }).obj (Opposite.op X))),
  (CategoryTheory.Hom.addEquivCongrRight e X) a =
    (AddMonCat.Hom.hom (AddMonCat.ofHom (CategoryTheory.IsAddMonHom.addMonoidHom e.hom X))) a
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
/-- Given an abelian sheaf `F`, this is the presheaf which sends `U`
to the `n`th Ext-group from the free abelian sheaf generated by the
presheaf of sets `yoneda.obj U` to `F`.  -/
CategoryTheory.Sheaf.cohomologyPresheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
        [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] →
          CategoryTheory.Sheaf J AddCommGrpCat → ℕ → CategoryTheory.Functor Cᵒᵖ AddCommGrpCat
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.piCongrRight_apply : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {ι : Type u_9} {M : ι → Type u_10} [inst_1 : (i : ι) → TopologicalSpace (M i)]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R₁ (M i)] {N : ι → Type u_11}
  [inst_4 : (i : ι) → TopologicalSpace (N i)] [inst_5 : (i : ι) → AddCommMonoid (N i)]
  [inst_6 : (i : ι) → Module R₁ (N i)] (f : (i : ι) → M i ≃L[R₁] N i) (m : (i : ι) → M i) (i : ι),
  (ContinuousLinearEquiv.piCongrRight f) m i = (f i) (m i)
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_fin_one : ∀ {α : Type u} (x : α) (u : Fin 0 → α), Matrix.vecCons x u = fun x_1 => x
-- Init.Core
gt_iff_lt : ∀ {α : Type u_1} [inst : LT α] {x y : α}, x > y ↔ y < x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Topology.IsEmbedding.aestronglyMeasurable_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ]
  {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace.PseudoMetrizableSpace β]
  [TopologicalSpace.PseudoMetrizableSpace γ] {g : β → γ} {f : α → β},
  Topology.IsEmbedding g →
    (MeasureTheory.AEStronglyMeasurable (fun x => g (f x)) μ ↔ MeasureTheory.AEStronglyMeasurable f μ)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- A semilinear isometric equivalence between two normed vector spaces,
denoted as `f : E ≃ₛₗᵢ[σ₁₂] E₂`.  -/
LinearIsometryEquiv : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring R₂] →
        (σ₁₂ : R →+* R₂) →
          {σ₂₁ : R₂ →+* R} →
            [RingHomInvPair σ₁₂ σ₂₁] →
              [RingHomInvPair σ₂₁ σ₁₂] →
                (E : Type u_11) →
                  (E₂ : Type u_12) →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] → [Module R E] → [Module R₂ E₂] → Type (max u_11 u_12)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The map `Cochain K L n → Cochain (K⟦a⟧) (L⟦a⟧) n`.  -/
CochainComplex.HomComplex.Cochain.shift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          CochainComplex.HomComplex.Cochain K L n →
            (a : ℤ) →
              CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K)
                ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_eq_zero : ∀ {R : Type u} [inst : Semiring R] {a : Polynomial R}, a.toFinsupp = 0 ↔ a = 0
-- Init.Data.List.MapIdx
List.mapIdx_eq_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {l' : List α_1} {l : List α},
  List.mapIdx f l = l' ↔ ∀ (i : ℕ), l'[i]? = Option.map (f i) l[i]?
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_union_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂).get k ⋯ = m₂.get k mem
-- Mathlib.Util.CountHeartbeats
/-- Given a `List Nat`, return the minimum, maximum, and standard deviation.
 -/
Mathlib.CountHeartbeats.variation : List ℕ → List ℕ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α},
  t.minKey? = some km → km ∈ t
-- Init.Core
eq_comm : ∀ {α : Sort u_1} {a b : α}, a = b ↔ b = a
-- Mathlib.Algebra.Lie.Abelian
LieAlgebra.instIsLieAbelianSubtypeMemLieIdealCenter : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  IsLieAbelian ↥(LieAlgebra.center R L)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
IsSelfAdjoint.commute_cfcHom : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra 𝕜 A] [inst_4 : TopologicalSpace A] [inst_5 : ContinuousFunctionalCalculus 𝕜 A p]
  [IsSemitopologicalRing A] [T2Space A] {a b : A} (ha : p a),
  IsSelfAdjoint a → Commute a b → ∀ (f : C(↑(spectrum 𝕜 a), 𝕜)), Commute ((cfcHom ha) f) b
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.mem_iInf : ∀ {M : Type u_1} [inst : Mul M] {ι : Sort u_3} {S : ι → Subsemigroup M} {x : M}, x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.toLinearMap_rankOne : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x : E) (y : F),
  ↑(((InnerProductSpace.rankOne 𝕜) x) y) = ((innerₛₗ 𝕜) y).smulRight x
-- Mathlib.Algebra.Category.BialgCat.Basic
/-- Typecheck a `BialgHom` as a morphism in `BialgCat R`.  -/
BialgCat.ofHom : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : Ring X] →
        [inst_2 : Ring Y] →
          [inst_3 : Bialgebra R X] → [inst_4 : Bialgebra R Y] → (X →ₐc[R] Y) → (BialgCat.of R X ⟶ BialgCat.of R Y)
-- Std.Time.Zoned.ZoneRules
/-- Returns the `TimeZone` in effect for this `RecurringRule` at the given `Timestamp`.

If no DST rule is defined, or if either transition rule is missing, the standard zone is returned
unconditionally. Otherwise the function computes the UTC timestamps at which DST starts and ends
for the year containing `tm`, and returns the DST zone when the timestamp falls inside the DST
interval (accounting for rules that wrap across a year boundary in the Southern Hemisphere).
 -/
Std.Time.TimeZone.RecurringRule.timezoneAt : Std.Time.TimeZone.RecurringRule → Std.Time.Timestamp → Std.Time.TimeZone
-- Mathlib.Combinatorics.SetFamily.FourFunctions
/-- Special case of the **Four Functions Theorem** when `s = t = univ`.  -/
four_functions_theorem_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : DistribLattice α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] [ExistsAddOfLE β] (f₁ f₂ f₃ f₄ : α → β) [inst_5 : Fintype α],
  0 ≤ f₁ →
    0 ≤ f₂ →
      0 ≤ f₃ →
        0 ≤ f₄ →
          (∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) → (∑ a, f₁ a) * ∑ a, f₂ a ≤ (∑ a, f₃ a) * ∑ a, f₄ a
-- Lean.Elab.Binders
Lean.Elab.Term.FunBinders.State.mk.sizeOf_spec : ∀ (fvars : Array Lean.Expr) (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances)
  (expectedType? : Option Lean.Expr),
  sizeOf { fvars := fvars, lctx := lctx, localInsts := localInsts, expectedType? := expectedType? } =
    1 + sizeOf fvars + sizeOf lctx + sizeOf localInsts + sizeOf expectedType?
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.lanUnit_desc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] (s : CategoryTheory.Bicategory.LeftExtension f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanUnit f g)
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.lanDesc s)) =
    s.unit
-- Std.Sync.CancellationToken
Std.instBEqCancellationReason : BEq Std.CancellationReason
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.continuous_pow : ∀ (n : ℕ), Continuous fun x => x ^ n
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.pi_sdiff_pi_subset`. -/
Set.pi_diff_pi_subset : ∀ {α : Type u_1} {π : α → Type u_12} (i : Set α) (s t : (a : α) → Set (π a)),
  i.pi s \ i.pi t ⊆ ⋃ a ∈ i, Function.eval a ⁻¹' (s a \ t a)
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.instOrdGCongrKey : Ord Mathlib.Tactic.GCongr.GCongrKey
-- Init.Data.String.TakeDrop
/-- Repeatedly increments a position in a string, as if by `String.Pos.Raw.next`, while the predicate
`p` returns `false` for the character at the position. Stops incrementing at the end of
the string or when `p` returns `true` for the current character.

Examples:

* `let s := "   a  "; (Pos.Raw.nextUntil s Char.isWhitespace 0).get s = ' '`

* `let s := "   a  "; (Pos.Raw.nextUntil s Char.isAlpha 0).get s = 'a'`

* `let s := "a  "; (Pos.Raw.nextUntil s Char.isWhitespace 0).get s = ' '`
 -/
String.Pos.Raw.nextUntil : String → (Char → Bool) → String.Pos.Raw → String.Pos.Raw
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.coneOfDiagramInitial_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {X : J} (tX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C),
  (CategoryTheory.Limits.coneOfDiagramInitial tX F).pt = F.obj X
-- Mathlib.Combinatorics.SetFamily.Intersecting
/-- An `L`-intersecting family remains `L`-intersecting under restriction to any subfamily.
 -/
Set.IsIntersectingOf.anti : ∀ {L : Set ℕ} {α : Type u_1} [inst : DecidableEq α] {𝒜 ℬ : Set (Finset α)},
  ℬ ⊆ 𝒜 → L.IsIntersectingOf 𝒜 → L.IsIntersectingOf ℬ
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.of.eq_1 : ∀ {α : Type u} [inst : Add α], AddMagma.FreeAddSemigroup.of = { toFun := Quot.mk (AddMagma.AssocRel α), map_add' := ⋯ }
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.adj_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C),
  T.adj.unit = { app := fun X => T.η.app X, naturality := ⋯ }
-- Mathlib.RingTheory.Ideal.Operations
/-- `Associates (Ideal R)` almost never has a decidable reducibility check.
We add a global instance that members of `Associates (Ideal R)` have decidable
reducibility, coming from the choice axiom, so that we don't have to provide
this as an arguments in lemma statements.  -/
Ideal.instDecidableIrreducibleAssociates : {R : Type u_1} → [inst : CommSemiring R] → (I : Associates (Ideal R)) → Decidable (Irreducible I)
-- Mathlib.Data.Finset.Powerset
Finset.pairwiseDisjoint_pair_insert : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] {a : α},
  a ∉ s → (↑s.powerset).PairwiseDisjoint fun t => {t, insert a t}
-- Mathlib.Tactic.Order.Graph.Basic
/-- Given a `≤`-graph `g`, finds a proof of `s ≤ t` using transitivity.  -/
Mathlib.Tactic.Order.Graph.buildTransitiveLeProof : Mathlib.Tactic.Order.Graph → ℕ → ℕ → Mathlib.Tactic.AtomM (Option Lean.Expr)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Cfg.mk.inj : ∀ {Γ : Type u_1} {Λ : Type u_2} {inst : Inhabited Γ} {q : Λ} {Tape : Turing.Tape Γ} {q_1 : Λ} {Tape_1 : Turing.Tape Γ},
  { q := q, Tape := Tape } = { q := q_1, Tape := Tape_1 } → q = q_1 ∧ Tape = Tape_1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegrable_iff_integrableOn_Ico_of_le : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ],
  a ≤ b →
    autoParam (‖f a‖ₑ ≠ ⊤) intervalIntegrable_iff_integrableOn_Ico_of_le._auto_1 →
      autoParam (‖f b‖ₑ ≠ ⊤) intervalIntegrable_iff_integrableOn_Ico_of_le._auto_3 →
        (IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Ico a b) μ)
-- Std.Data.HashSet.Lemmas
Std.HashSet.toList_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {f : α → Bool},
  (Std.HashSet.filter f m).toList.Perm (List.filter f m.toList)
-- Std.Time.Zoned.Database.Basic
/-- Converts a Boolean value to a corresponding `StdWall` type.
 -/
Std.Time.TimeZone.convertWall : Bool → Std.Time.TimeZone.StdWall
-- Mathlib.Data.Fin.Parity
/-- In `Fin n`, all elements are even for odd `n`,
otherwise an element is even iff its `Fin.val` value is even.  -/
Fin.even_iff : ∀ {n : ℕ} {k : Fin n}, Even k ↔ Odd n ∨ Even ↑k
-- Mathlib.Analysis.RCLike.Basic
RCLike.continuous_normSq : ∀ {K : Type u_1} [inst : RCLike K], Continuous ⇑RCLike.normSq
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_presheafObjObjIso_hom : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) (X : C)
  (i : (data X).I₀),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ ((data X).f i))
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso data G₀ ((data X).X i)).hom =
    CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addX_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ≠ Q 0 * P 2 →
            W.addX P Q / W.addZ P Q =
              W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.strictMono_cast : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α],
  StrictMono Nat.cast
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
/-- The path `t ↦ expUnitary (t • argSelfAdjoint (v * star u)) * u`
from `u : unitary A` to `v` when `‖v - u‖ < 2`.  -/
Unitary.path : {A : Type u_1} → [inst : CStarAlgebra A] → (u v : ↥(unitary A)) → ‖↑v - ↑u‖ < 2 → Path u v
-- Lean.Elab.DocString
/-- The arguments it should receive, as a string.  -/
Lean.Doc.CodeBlockSuggestion.args : Lean.Doc.CodeBlockSuggestion → Option String
-- Init.Data.List.ToArray
List.eraseP_toArray : ∀ {α : Type u_1} {as : List α} {p : α → Bool}, as.toArray.eraseP p = (List.eraseP p as).toArray
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapComp'_inv_naturality : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (hfg : CategoryTheory.CategoryStruct.comp f g = fg) (a : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F.map g).toFunctor.map ((F.map f).toFunctor.map a))
      ((F.mapComp' f g fg hfg).inv.toNatTrans.app Y) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.toNatTrans.app X) ((F.map fg).toFunctor.map a)
-- Std.Time.Date.Unit.Month
Std.Time.Month.instLTOrdinal : LT Std.Time.Month.Ordinal
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- If the union of a.e.-disjoint null-measurable sets has finite measure, then there are only
countably many members of the union whose measure is positive.  -/
MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ : ∀ {α : Type u_1} {ι : Type u_4} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) →
    Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) As) → μ (⋃ i, As i) ≠ ⊤ → {i | 0 < μ (As i)}.Countable
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.pow_sub' : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (A : Matrix n' n' R) {m n : ℕ}, IsUnit A.det → n ≤ m → A ^ (m - n) = A ^ m * (A ^ n)⁻¹
-- Std.Http.Data.Body.Stream
/-- Known size of the stream if available.
 -/
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.State.knownSize : Std.Http.Body.Channel.State✝ → Option Std.Http.Body.Length
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableSMul_opposite_of_mul : ∀ {M : Type u_2} [inst : Mul M] [inst_1 : MeasurableSpace M] [MeasurableMul M], MeasurableSMul Mᵐᵒᵖ M
-- Init.Prelude
/-- Checks whether two terms of a type are equal using the type's `DecidableEq` instance.
 -/
decEq : {α : Sort u} → [inst : DecidableEq α] → (a b : α) → Decidable (a = b)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The trifunctor `X₁ X₂ X₃ ↦ X₁ ⊗ (X₂ ⊗ X₃)`  -/
CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃' : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C C))
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_eq_none : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a : α},
  a ∉ m → m.get? a = none
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- A basic trapezoidal equivalent to `IntervalIntegral.sum_integral_adjacent_intervals`. More
general theorems are certainly possible, but many of them can be derived from repeated applications
of this one.  -/
sum_trapezoidal_integral_adjacent_intervals : ∀ {f : ℝ → ℝ} {N : ℕ} {a h : ℝ},
  0 < N →
    ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + ↑i * h) (a + (↑i + 1) * h) =
      trapezoidal_integral f N a (a + ↑N * h)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
_private.Mathlib.CategoryTheory.Monoidal.Free.Basic.0.CategoryTheory.termF : Lean.ParserDescr
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- The underlying type of the free groupoid on a category,
defined by quotienting the free groupoid on the underlying quiver of `C`
by the relation that promotes the prefunctor `C ⥤q FreeGroupoid C` into a functor
`C ⥤ Quotient (FreeGroupoid.homRel C)`.  -/
CategoryTheory.FreeGroupoid : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type u
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.CotangentSpace.map.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f : P.Hom P'),
  Algebra.Extension.CotangentSpace.map f =
    LinearMap.liftBaseChange S
      (↑P.Ring ((TensorProduct.mk P'.Ring S' Ω[P'.Ring⁄R']) 1) ∘ₗ KaehlerDifferential.map R R' P.Ring P'.Ring)
-- Mathlib.Data.FinEnum
/-- A type indexable by `Fin 0` is empty and vice versa.  -/
FinEnum.card_eq_zero_iff : ∀ {α : Type u} [inst : FinEnum α], FinEnum.card α = 0 ↔ IsEmpty α
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- Composition of morphisms in the constructed localized category
for a morphism property that has left calculus of fractions.  -/
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      [W.HasLeftCalculusOfFractions] →
        {X Y Z : C} →
          CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y →
            CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W Y Z →
              CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Z
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.ext : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (u v : SpecialLinearGroup R V), (∀ (x : V), (fun x => ↑u x) x = (fun x => ↑v x) x) → u = v
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard_eq_filter : ∀ {α : Type u_1} {n : ℕ} {s : Finset α}, Finset.powersetCard n s = {x ∈ s.powerset | x.card = n}
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.η_hom : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G],
  Rep.Hom.hom (CategoryTheory.Functor.OplaxMonoidal.η (Rep.linearization k G)) = Representation.LinearizeMonoidal.η k G
-- Init.Data.UInt.Bitwise
UInt16.left_le_or : ∀ {a b : UInt16}, a ≤ a ||| b
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalClosure_idempotent : ∀ {G : Type u_1} [inst : Group G] {s : Set G},
  Subgroup.normalClosure ↑(Subgroup.normalClosure s) = Subgroup.normalClosure s