mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.comp_lift_id_left : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {a b c : 𝒳} {S T : 𝒮} (f : S ⟶ T) (ψ : b ⟶ c) [p.IsHomLift f ψ] (φ : a ⟶ b)
  [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ], p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ ψ)
-- Mathlib.Data.Finset.Defs
Finset.le_eq_subset : ∀ {α : Type u_1}, (fun x1 x2 => x1 ⊆ x2) = fun x1 x2 => x1 ⊆ x2
-- Mathlib.Topology.Algebra.Module.Complement
/-- If `p` and `q` are topological complements and `q` is closed, then `p` is Hausdorff.  -/
Submodule.IsTopCompl.t2Space : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [IsTopologicalAddGroup M],
  Submodule.IsTopCompl p q → IsClosed ↑q → T2Space ↥p
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.lipschitzWith_addEquiv : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A], LipschitzWith 2 ⇑(Unitization.addEquiv 𝕜 A)
-- Mathlib.Data.Finset.Sym
Finset.sym2_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), m.toFinset.sym2 = m.sym2.toFinset
-- Init.Classical
/-- the axiom of choice  -/
Classical.axiomOfChoice : ∀ {α : Sort u} {β : α → Sort v} {r : (x : α) → β x → Prop}, (∀ (x : α), ∃ y, r x y) → ∃ f, ∀ (x : α), r x (f x)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.compl_mk : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} (a : α) (ha : a ∈ L), ⟨a, ha⟩ᶜ = ⟨aᶜ, ⋯⟩
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.Iter.Equiv.refl : ∀ {β α : Type w} [inst : Std.Iterator α Id β] (it : Std.Iter β), it.Equiv it
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Given an exact pairing on `Y Y'`,
we get a bijection on hom-sets `(X ⊗ Y ⟶ Z) ≃ (X ⟶ Z ⊗ Y')`
by "pulling the string on the right" up or down.
 -/
CategoryTheory.tensorRightHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y Y' Z : C) →
        [CategoryTheory.ExactPairing Y Y'] →
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) ≃
            (X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y')
-- Mathlib.Algebra.Homology.Homotopy
/-- `f` is homotopic to `g` iff `g` is homotopic to `f`.  -/
Homotopy.symm : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → {f g : C ⟶ D} → Homotopy f g → Homotopy g f
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.restrictSource.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f f_1 : X.PartialIso Y) (e_f : f = f_1) (U U_1 : X.Opens) (e_U : U = U_1)
  (hU : Dense ↑U) (hU' : U ≤ f.source), f.restrictSource U hU hU' = f_1.restrictSource U_1 ⋯ ⋯
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.ratio_refl : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X], Dilation.ratio (DilationEquiv.refl X) = 1
-- Lean.Elab.MutualDef
/-- Create auxiliary local declarations `fs` for the given headers using their `shortDeclName` and `type`, given headers, and execute `k fs`.
The new free variables are tagged as `auxDecl`.
Remark: `fs.size = headers.size`.
 -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.withFunLocalDecls : {α : Type} → Array Lean.Elab.DefViewElabHeader → (Array Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Init.Data.Vector.Basic
instDecidableEqVector.decEq : {α : Type u_1} → {n : ℕ} → [DecidableEq α] → (x x_1 : Vector α n) → Decidable (x = x_1)
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.span_preimage_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {R₂ : Type u_3}
  {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {s : Set M₂},
  s.Nonempty → s ⊆ ↑f.range → Submodule.span R (⇑f ⁻¹' s) = Submodule.comap f (Submodule.span R₂ s)
-- Mathlib.Topology.Order
le_of_nhds_le_nhds : ∀ {α : Type u_1} {t₁ t₂ : TopologicalSpace α}, (∀ (x : α), nhds x ≤ nhds x) → t₁ ≤ t₂
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_apply_same : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)),
  i.insertNth x p i = x
-- Mathlib.Algebra.Group.ULift
ULift.monoid.eq_1 : ∀ {α : Type u} [inst : Monoid α], ULift.monoid = Function.Injective.monoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯
-- Mathlib.Logic.Equiv.Set
Equiv.setOfPred_apply_symm_eq_image_setOfPred : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (p : α → Prop), {b | p (e.symm b)} = ⇑e '' {a | p a}
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange_comp : ∀ {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β i)]
  [inst_1 : (i : ι) → Zero (β₁ i)] [inst_2 : (i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ i → β₂ i)
  (f₂ : (i : ι) → β i → β₁ i) (hf : ∀ (i : ι), f i 0 = 0) (hf₂ : ∀ (i : ι), f₂ i 0 = 0)
  (h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0) (g : Π₀ (i : ι), β i),
  DFinsupp.mapRange (fun i => f i ∘ f₂ i) h g = DFinsupp.mapRange f hf (DFinsupp.mapRange f₂ hf₂ g)
-- Mathlib.Data.Num.Lemmas
Num.pred.eq_1 : Num.zero.pred = 0
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.toUpper_lt_toUpper : ∀ {α : Type u_1} [inst : Preorder α] {x y : α}, Topology.WithUpper.toUpper x < Topology.WithUpper.toUpper y ↔ x < y
-- Lean.Widget.Diff
/-- A marker for a point in the expression where a subexpression has been inserted.

NOTE: in the future we may add other tags.
 -/
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiffTag : Type
-- Mathlib.LinearAlgebra.Alternating.Curry
/-- Currying with the same element twice gives the zero map.  -/
AlternatingMap.curryLeft_same : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin n.succ.succ]→ₗ[R] N)
  (m : M), (f.curryLeft m).curryLeft m = 0
-- Init.Data.SInt.Lemmas
Int32.mul_one : ∀ (a : Int32), a * 1 = a
-- Std.Data.TreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
less than or equal to the given key.
 -/
Std.TreeMap.getEntryLE : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.TreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isLE = true) → α × β
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vadd_finset_subset_vadd_finset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {s t : Finset β}
  {a : α}, a +ᵥ s ⊆ a +ᵥ t ↔ s ⊆ t
-- Mathlib.Logic.Equiv.Defs
Equiv.conj_comp : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (f₁ f₂ : α → α), e.conj (f₁ ∘ f₂) = e.conj f₁ ∘ e.conj f₂
-- Mathlib.AlgebraicGeometry.Sites.Small
AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] {X : CategoryTheory.Over S}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X.left)
  [inst_1 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰],
  (CategoryTheory.Sieve.overEquiv X) (CategoryTheory.Sieve.generate 𝒰.toPresieveOver) =
    CategoryTheory.Sieve.ofArrows 𝒰.X 𝒰.f
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instIsTopologicalAddGroup : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G],
  IsTopologicalAddGroup (SeparationQuotient G)
-- Mathlib.Algebra.Category.ModuleCat.InjectiveDimension
_private.Mathlib.Algebra.Category.ModuleCat.InjectiveDimension.0.ModuleCat.hasInjectiveDimensionLE_iff_of_semiLinearEquiv_aux : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] {R' : Type u'} [inst_2 : Ring R'] (eR : R ≃+* R') [Small.{v, u'} R']
  {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N) (n : ℕ),
  CategoryTheory.HasInjectiveDimensionLE M n ↔ CategoryTheory.HasInjectiveDimensionLE N n
-- Lean.Syntax
Lean.Syntax.Range.overlaps : Lean.Syntax.Range → Lean.Syntax.Range → optParam Bool false → optParam Bool false → Bool
-- Init.Data.Nat.Lcm
Nat.lcm_eq_right_iff_dvd : ∀ {m n : ℕ}, m.lcm n = n ↔ m ∣ n
-- Mathlib.Order.BooleanAlgebra.Set
Set.pair_sdiff_right : ∀ {α : Type u_1} {a b : α}, a ≠ b → {a, b} \ {b} = {a}
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.continuous_symm : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), Continuous ⇑h.symm
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- Given a point in an affine subspace, a result of subtracting that point on the left is in the
direction if and only if the other point is in the subspace.  -/
AffineSubspace.vsub_left_mem_direction_iff_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P}, p ∈ s → ∀ (p₂ : P), p -ᵥ p₂ ∈ s.direction ↔ p₂ ∈ s
-- Mathlib.Analysis.Normed.Group.Basic
dist_eq_norm_div' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (a b : E), dist a b = ‖b / a‖
-- Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
/-- If `f` is `n` times continuously differentiable at `x`, then the `n`th iterated Fréchet derivative
with respect to `𝕜` equals scalar restriction of the `n`th iterated Fréchet derivative with respect
to `𝕜'`.
 -/
ContDiffAt.restrictScalars_iteratedFDeriv : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {x : E} {f : E → F} {n : ℕ},
  ContDiffAt 𝕜' (↑n) f x →
    (ContinuousMultilinearMap.restrictScalars 𝕜 ∘ iteratedFDeriv 𝕜' n f) x = iteratedFDeriv 𝕜 n f x
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β] (f : SupBotHom α β)
  (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Init.Data.List.Range
List.range_one : List.range 1 = [0]
-- Mathlib.Analysis.CStarAlgebra.Spectrum
CStarAlgebra.sqrt_toReal_spectralRadius_star_mul_self_eq_norm : ∀ {A : Type u_1} [inst : CStarAlgebra A] (a : A), √(spectralRadius ℂ (star a * a)).toReal = ‖a‖
-- Mathlib.FieldTheory.AbelRuffini
solvableByRad_le_algClosure : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  solvableByRad F E ≤ algebraicClosure F E
-- Mathlib.RingTheory.Algebraic.Basic
inv_eq_of_root_of_coeff_zero_ne_zero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L} {p : Polynomial K},
  (Polynomial.aeval x) p = 0 → p.coeff 0 ≠ 0 → x⁻¹ = -((Polynomial.aeval x) p.divX / (algebraMap K L) (p.coeff 0))
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- The seminorm of a scalar multiplication is the product of the absolute value of the scalar
and the original seminorm.  -/
AlgebraNormClass.map_smul_eq_mul : ∀ {F : Type u_1} {R : outParam (Type u_2)} {inst : SeminormedCommRing R} {S : outParam (Type u_3)} {inst_1 : Ring S}
  {inst_2 : Algebra R S} {inst_3 : FunLike F S ℝ} [self : AlgebraNormClass F R S] (f : F) (a : R) (x : S),
  f (a • x) = ‖a‖ * f x
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.cmp.match_1.eq_4 : ∀ (motive : ONote → ONote → Sort u_1) (e₁ : ONote) (n₁ : ℕ+) (a₁ e₂ : ONote) (n₂ : ℕ+) (a₂ : ONote)
  (h_1 : Unit → motive ONote.zero ONote.zero) (h_2 : (x : ONote) → motive x ONote.zero)
  (h_3 : (x : ONote) → motive ONote.zero x)
  (h_4 :
    (_o₁ e₁ : ONote) →
      (n₁ : ℕ+) →
        (a₁ : ONote) →
          _o₁ = e₁.oadd n₁ a₁ →
            (_o₂ e₂ : ONote) → (n₂ : ℕ+) → (a₂ : ONote) → _o₂ = e₂.oadd n₂ a₂ → motive (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)),
  (match e₁.oadd n₁ a₁, e₂.oadd n₂ a₂ with
    | ONote.zero, ONote.zero => h_1 ()
    | x, ONote.zero => h_2 x
    | ONote.zero, x => h_3 x
    | _o₁@h:(e₁.oadd n₁ a₁), _o₂@h_5:(e₂.oadd n₂ a₂) => h_4 _o₁ e₁ n₁ a₁ h _o₂ e₂ n₂ a₂ h_5) =
    h_4 (e₁.oadd n₁ a₁) e₁ n₁ a₁ ⋯ (e₂.oadd n₂ a₂) e₂ n₂ a₂ ⋯
-- Batteries.Data.Float.Lemmas
Float.beq_iff_ne_nan_and_eq : ∀ {f f' : Float}, (f == f') = true ↔ f ≠ Float.nan ∧ f' ≠ Float.nan ∧ (f = f' ∨ f = 0 ∧ f' = -0 ∨ f = -0 ∧ f' = 0)
-- Mathlib.Probability.Kernel.Composition.CompMap
ProbabilityTheory.Kernel.comp_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  (η : ProbabilityTheory.Kernel γ δ) {f : β → γ} (hf : Measurable f), η.comp (κ.map f) = (η.comap f hf).comp κ
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `𝓕 : ι → β → α` is uniformly equicontinuous on `S` iff the function
`swap 𝓕 : β → ι → α` is uniformly continuous on `S`
*when `ι → α` is equipped with the uniform structure of uniform convergence*. This is very useful
for developing the equicontinuity API, but it should not be used directly for other purposes.  -/
uniformEquicontinuousOn_iff_uniformContinuousOn : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α} {S : Set β},
  UniformEquicontinuousOn F S ↔ UniformContinuousOn (⇑UniformFun.ofFun ∘ Function.swap F) S
-- Mathlib.Tactic.DeriveCountable
/-- The `encode` function is injective. Used internally by the `Countable` deriving handler.  -/
Mathlib.Deriving.Countable.encode_injective : ∀ {α : Sort u_1} [inst : Countable α], Function.Injective Mathlib.Deriving.Countable.encode
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.sum : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α}
  {E_1 : ℕ → α},
  Monotone E_1 →
    ∀ {n : ℕ},
      (∀ (i : ℕ), 0 < i → i < n → E_1 i ∈ s) →
        ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Set.Icc (E_1 i) (E_1 (i + 1))) =
          eVariationOn f (s ∩ Set.Icc (E_1 0) (E_1 n))
-- Init.Data.Nat.Div.Basic
_private.Init.Data.Nat.Div.Basic.0.Nat.div.go.fuel_congr : ∀ (x y fuel1 fuel2 : ℕ) (hy : 0 < y) (h1 : x < fuel1) (h2 : x < fuel2),
  Nat.div.go y hy fuel1 x h1 = Nat.div.go y hy fuel2 x h2
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeConstantResult.mk.injEq : ∀ (snap? : Option Lean.Language.SnapshotTree) (error? : Option Lean.Exception)
  (snap?_1 : Option Lean.Language.SnapshotTree) (error?_1 : Option Lean.Exception),
  ({ snap? := snap?, error? := error? } = { snap? := snap?_1, error? := error?_1 }) =
    (snap? = snap?_1 ∧ error? = error?_1)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.single_eq_zero_iff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ} {r : R},
  (HahnSeries.single a) r = 0 ↔ r = 0
-- Lean.Elab.PreDefinition.WF.Fix
Lean.Elab.WF.solveDecreasingGoals : Array Lean.Name → Lean.Meta.ArgsPacker → Array (Option Lean.Elab.DecreasingBy) → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Complex.hasSum_taylorSeries_neg_log' : ∀ {z : ℂ}, ‖z‖ < 1 → HasSum (fun n => z ^ (n + 1) / (↑n + 1)) (-Complex.log (1 - z))
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.lie_of_of_ne : ∀ {ι : Type v} (L : ι → Type w) [inst : (i : ι) → LieRing (L i)] [inst_1 : DecidableEq ι] {i j : ι},
  i ≠ j → ∀ (x : L i) (y : L j), ⁅(DirectSum.of L i) x, (DirectSum.of L j) y⁆ = 0
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_left_inj' : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, c ≠ 0 → (a / c = b / c ↔ a = b)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.map_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} D]
  [inst_3 : CategoryTheory.Preadditive D] (z z' : CochainComplex.HomComplex.Cochain K L n)
  (Φ : CategoryTheory.Functor C D) [inst_4 : Φ.Additive], (z - z').map Φ = z.map Φ - z'.map Φ
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.isRepresentable_comp_uliftFunctor_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)},
  (F.comp CategoryTheory.uliftFunctor.{w, v}).IsRepresentable ↔ F.IsRepresentable
-- Mathlib.MeasureTheory.Order.Group.Lattice
AEMeasurable.negPart : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : AddGroup α] [inst_2 : MeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} [MeasurableNeg α] {μ : MeasureTheory.Measure β} [MeasurableSup α],
  AEMeasurable f μ → AEMeasurable (fun x => (f x)⁻) μ
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp'_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : F.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃))
      (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f hf) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃))
        (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯) h))
-- Init.Data.Array.Zip
Array.unzip_zip : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β}, as.size = bs.size → (as.zip bs).unzip = (as, bs)
-- Mathlib.Order.Filter.Defs
/-- `f.Eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in atTop, p x`
means that `p` holds true for sufficiently large `x`.  -/
Filter.«term∀ᶠ_In_,_» : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- Constructor for edges in a simplicial set.  -/
SSet.Edge.mk : {X : SSet} →
  {x₀ x₁ : X.obj (Opposite.op { len := 0 })} →
    (edge : X.obj (Opposite.op { len := 1 })) →
      autoParam ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) edge = x₀) _auto_31✝ →
        autoParam ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) edge = x₁) _auto_33✝ →
          SSet.Edge x₀ x₁
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
Measurable.mono : ∀ {α : Type u_1} {β : Type u_2} {ma ma' : MeasurableSpace α} {mb mb' : MeasurableSpace β} {f : α → β},
  Measurable f → ma ≤ ma' → mb' ≤ mb → Measurable f
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.toAlgHom_taylorEquiv : ∀ {R : Type u_1} [inst : CommRing R] (r : R), ↑(Polynomial.taylorEquiv r) = Polynomial.taylorAlgHom r
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- If `P` is a sheaf for every pullback of the sieve `S`, then `P` is a sheaf for any presieve which
contains `S`.
This is closely related to [Elephant] C2.1.6.
 -/
CategoryTheory.Presieve.isSheafFor_subsieve : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w))
  {S : CategoryTheory.Sieve X} {R : CategoryTheory.Presieve X},
  S.arrows ≤ R →
    (∀ ⦃Y : C⦄ (f : Y ⟶ X), CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows) →
      CategoryTheory.Presieve.IsSheafFor P R
-- Mathlib.Data.Set.Functor
Set.image_val_subset : ∀ {α : Type u} {β : Set α} {γ : Set ↑β}, Subtype.val '' γ ⊆ β
-- Mathlib.RingTheory.Localization.FractionRing
algebraMap_injective_of_field_isFractionRing : ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S] (K : Type u_6)
  (L : Type u_7) [inst_3 : Field K] [inst_4 : Semiring L] [Nontrivial L] [inst_6 : Algebra R K] [IsFractionRing R K]
  [inst_8 : Algebra S L] [inst_9 : Algebra K L] [inst_10 : Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L],
  Function.Injective ⇑(algebraMap R S)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {c c' : C} {d d' : D} (f : d ⟶ d') (g : c ⟶ c'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d' g)
-- Mathlib.Order.Filter.Cofinite
Finset.eventually_cofinite_notMem : ∀ {α : Type u_2} (s : Finset α), ∀ᶠ (x : α) in Filter.cofinite, x ∉ s
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `L/K` is finite and normal, then `spectralNorm K L` is power-multiplicative.
See also the more general result `isPowMul_spectralNorm`.  -/
isPowMul_spectralNorm_of_finiteDimensional_normal : ∀ (K : Type u_2) [inst : NormedField K] (L : Type u_3) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K], IsPowMul (spectralNorm K L)
-- Mathlib.RingTheory.Valuation.Basic
/-- For fields, being nontrivial is equivalent to the existence of a unit with valuation
not equal to `1`.  -/
Valuation.isNontrivial_iff_exists_unit : ∀ {Γ₀ : Type u_4} [inst : LinearOrderedCommMonoidWithZero Γ₀] {K : Type u_7} [inst_1 : DivisionRing K]
  {w : Valuation K Γ₀}, w.IsNontrivial ↔ ∃ x, w ↑x ≠ 1
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The object in the fiber of the base object.  -/
CategoryTheory.Pseudofunctor.Grothendieck.fiber : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
      (self : F.Grothendieck) → ↑(F.obj { as := self.base })
-- Init.Data.BitVec.BasicAux
BitVec.instAdd : {n : ℕ} → Add (BitVec n)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.LazyEntry.mk.sizeOf_spec : ∀ (previous : Option Lean.Meta.RefinedDiscrTree.ExprInfo) (stack : List Lean.Meta.RefinedDiscrTree.StackEntry)
  (mctx : Lean.MetavarContext) (labelledStars? : Option (Array Lean.MVarId))
  (computedKeys : List Lean.Meta.RefinedDiscrTree.Key),
  sizeOf
      { previous := previous, stack := stack, mctx := mctx, labelledStars? := labelledStars?,
        computedKeys := computedKeys } =
    1 + sizeOf previous + sizeOf stack + sizeOf mctx + sizeOf labelledStars? + sizeOf computedKeys
-- Mathlib.Tactic.Core
/-- `repeat1 tac` applies `tac` to main goal at least once. If the application succeeds,
the tactic is applied recursively to the generated subgoals until it eventually fails.
 -/
Mathlib.Tactic.tacticRepeat1_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.Candidate.π.eq_1 : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts V] {u v : CategoryTheory.Arrow V} (f : u ⟶ v),
  CategoryTheory.Preadditive.RightFreyd.Candidate.π f =
    CategoryTheory.Arrow.homMk CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.id v.right) ⋯