mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.property_map : ∀ {m : Type w → Type w'} [inst : Functor m] {α : Type u} {β : Type v} {x : Std.Iterators.HetT m α} {f : α → β} {b : β},
  (Std.Iterators.HetT.map f x).Property b ↔ ∃ a, f a = b ∧ x.Property a
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.algebraPreadditive_homGroup_neg_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive] (A₁ A₂ : CategoryTheory.Endofunctor.Algebra F) (α : A₁ ⟶ A₂),
  (-α).f = -α.f
-- Mathlib.RingTheory.PowerSeries.Trunc
/-- The function `coeff n : R⟦X⟧ → R` is continuous. I.e. `coeff n f` depends only on a sufficiently
long truncation of the power series `f`.  -/
PowerSeries.coeff_coe_trunc_of_lt : ∀ {R : Type u_2} [inst : CommSemiring R] {n m : ℕ} {f : PowerSeries R},
  n < m → (PowerSeries.coeff n) ↑((PowerSeries.trunc m) f) = (PowerSeries.coeff n) f
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneLeftOpOfCocone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Limits.coneLeftOpOfCocone c = { pt := Opposite.unop c.pt, π := CategoryTheory.NatTrans.leftOp c.ι }
-- Mathlib.Algebra.Ring.Pointwise.Finset
/-- `Finset α` has distributive negation if `α` has.  -/
Finset.distribNeg : {α : Type u_1} → [inst : DecidableEq α] → [inst_1 : Mul α] → [HasDistribNeg α] → HasDistribNeg (Finset α)
-- Std.Time.Date.Unit.Day
/-- Creates an `Offset` from a natural number.
 -/
Std.Time.Day.Offset.ofNat : ℕ → Std.Time.Day.Offset
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.compLpₗ.congr_simp : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] (L L_1 : E →SL[σ] F),
  L = L_1 → ContinuousLinearMap.compLpₗ p μ L = ContinuousLinearMap.compLpₗ p μ L_1
-- Mathlib.LinearAlgebra.Trace
Matrix.toLinAlgEquiv'.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  Matrix.toLinAlgEquiv' = LinearMap.toMatrixAlgEquiv'.symm
-- Mathlib.Data.Finset.Card
Finset.card_union_add_card_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t).card + (s ∩ t).card = s.card + t.card
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_shift : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F), p.shift.radius = p.radius
-- Mathlib.Logic.Relator
/-- A relation is "bi-total" if it is both right total and left total.  -/
Relator.BiTotal : {α : Sort u₁} → {β : Sort u₂} → (α → β → Prop) → Prop
-- Mathlib.Algebra.Lie.Basic
LieEquiv.symm_bijective : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂], Function.Bijective LieEquiv.symm
-- Mathlib.Topology.NhdsWithin
Filter.Tendsto.piecewise_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f g : α → β} {t : Set α}
  [inst_1 : (x : α) → Decidable (x ∈ t)] {a : α} {s : Set α} {l : Filter β},
  Filter.Tendsto f (nhdsWithin a (s ∩ t)) l →
    Filter.Tendsto g (nhdsWithin a (s ∩ tᶜ)) l → Filter.Tendsto (t.piecewise f g) (nhdsWithin a s) l
-- Mathlib.Data.Matrix.Basic
AddMonoidHom.mapMatrix_sub : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [inst : AddZeroClass α] [inst_1 : AddCommGroup β]
  (f g : α →+ β), (f - g).mapMatrix = f.mapMatrix - g.mapMatrix
-- Mathlib.GroupTheory.FreeGroup.Orbit
FreeGroup.startsWith_mk_mul : ∀ {α : Type u_1} [inst : DecidableEq α] {w : α × Bool},
  ∀ g ∉ FreeGroup.startsWith (w.1, !w.2), FreeGroup.mk [w] * g ∈ FreeGroup.startsWith w
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.coe_nonneg : ∀ {T : Type u_1} [inst : Ring T] [inst_1 : PartialOrder T] [inst_2 : IsOrderedRing T],
  ↑(RingCone.nonneg T) = {x | 0 ≤ x}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.contains t.minKey! = true
-- Mathlib.NumberTheory.ADEInequality
/-- `E7 := {2,3,4}` is a `Multiset ℕ+`
that is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.

This solution is related to the Dynkin diagrams $E_7$.  -/
ADEInequality.E7 : Multiset ℕ+
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
IsCovariantDerivativeOn.mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V]
  {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {s t : Set M},
  IsCovariantDerivativeOn F cov t → s ⊆ t → IsCovariantDerivativeOn F cov s
-- Lean.Meta.Eval
Lean.Meta.evalExpr : (α : Type) →
  Lean.Expr → Lean.Expr → optParam Lean.DefinitionSafety Lean.DefinitionSafety.safe → optParam Bool true → Lean.MetaM α
-- Mathlib.RingTheory.QuotSMulTop
QuotSMulTop.map_id : ∀ {R : Type u_2} [inst : CommRing R] (r : R) (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (QuotSMulTop.map r) LinearMap.id = LinearMap.id
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.neg.congr_simp : ∀ (R : Type u_1) [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : ContinuousNeg M], ContinuousLinearEquiv.neg R = ContinuousLinearEquiv.neg R
-- Lean.Meta.Closure
Lean.Meta.Closure.pickNextToProcess? : Lean.Meta.Closure.ClosureM (Option Lean.Meta.Closure.ToProcessElement)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- `padicValRat p 0` is `0` for any `p`.  -/
padicValRat.zero : ∀ {p : ℕ}, padicValRat p 0 = 0
-- Init.Grind.Offset
Lean.Grind.Nat.lo_eq_false_of_lo : ∀ (u v k₁ k₂ : ℕ), Lean.Grind.isLt 0 (k₁ + k₂) = true → u + k₁ ≤ v → (v + k₂ ≤ u) = False
-- Mathlib.Data.Rat.Cast.Defs
/-- If monoid with zero homs `f` and `g` from `ℚ` agree on the integers then they are equal.

See note [partially-applied ext lemmas] for why `comp` is used here.  -/
MonoidWithZeroHomClass.ext_rat : ∀ {M₀ : Type u_5} [inst : MonoidWithZero M₀] {f g : ℚ →*₀ M₀},
  f.comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ)) = g.comp (MonoidWithZeroHom.ofClass (Int.castRingHom ℚ)) →
    f = g
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.ofProp_meet_le_right : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {Q R : l} {φ : Prop},
  (φ → Lean.Order.PartialOrder.rel Q R) →
    Lean.Order.PartialOrder.rel (Lean.Order.meet Q (Lean.Order.CompleteLattice.ofProp φ)) R
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `lt_of_lt_of_antisymmRel`. -/
LT.lt.trans_antisymmRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α], a < b → AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → a < c
-- Mathlib.Algebra.Polynomial.Laurent
/-- Given a ring homomorphism `f : R →+* S` and a unit `x` in `S`, the induced homomorphism
`R[T;T⁻¹] →+* S` sending `T` to `x` and `T⁻¹` to `x⁻¹`.  -/
LaurentPolynomial.eval₂ : {R : Type u_1} →
  [inst : CommSemiring R] → {S : Type u_3} → [inst_1 : CommSemiring S] → (R →+* S) → Sˣ → LaurentPolynomial R →+* S
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.map_id : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R],
  Matrix.GeneralLinearGroup.map (RingHom.id R) = MonoidHom.id (GL n R)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffAt.prodMk_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {F' : Type u_11} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F'] {x : M}
  {n : WithTop ℕ∞} {f : M → E'} {g : M → F'},
  ContMDiffAt I (modelWithCornersSelf 𝕜 E') n f x →
    ContMDiffAt I (modelWithCornersSelf 𝕜 F') n g x →
      ContMDiffAt I (modelWithCornersSelf 𝕜 (E' × F')) n (fun x => (f x, g x)) x
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.InducedCategory.homLinearEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type w}
  [inst_2 : Semiring R] [inst_3 : CategoryTheory.Linear R C] {D : Type u'} {F : D → C}
  {X Y : CategoryTheory.InducedCategory C F} (a : X ⟶ Y), CategoryTheory.InducedCategory.homLinearEquiv a = a.hom
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.LawfulForwardPattern.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat],
  (∀ {s : String.Slice} (h : s.isEmpty = false),
      String.Slice.Pattern.ForwardPattern.skipPrefixOfNonempty? pat s h =
        String.Slice.Pattern.ForwardPattern.skipPrefix? pat s) →
    (∀ (s : String.Slice),
        String.Slice.Pattern.ForwardPattern.startsWith pat s =
          (String.Slice.Pattern.ForwardPattern.skipPrefix? pat s).isSome) →
      String.Slice.Pattern.LawfulForwardPattern pat
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.instIsStrictlySupportedTruncGE_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] {ι'' : Type u_4} {c'' : ComplexShape ι''} (e' : c''.Embedding c')
  [K.IsStrictlySupported e'], (K.truncGE e).IsStrictlySupported e'
-- Mathlib.Analysis.Seminorm
/-- Auxiliary lemma to show that the infimum of seminorms is well-defined.  -/
Seminorm.bddBelow_range_add : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {p q : Seminorm 𝕜 E} {x : E}, BddBelow (Set.range fun u => p u + q (x - u))
-- Mathlib.Order.Category.BoolAlg
BoolAlg.coe_comp : ∀ {X Y Z : BoolAlg} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Data.Finset.Sort
Finset.instRepr : {α : Type u_1} → [Repr α] → Repr (Finset α)
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.qsmul_of_nonneg : ∀ {M : Type u_2} [inst : AddCommGroup M] {a : ℚ} (h : 0 ≤ a) (x : DivisibleHull M),
  a • x =
    (have this := ⟨a, h⟩;
      this) •
      x
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.denote.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Mon → Sort u_1) (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit)
  (h_2 : (p : Lean.Grind.CommRing.Power) → (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m)),
  (match Lean.Grind.CommRing.Mon.unit with
    | Lean.Grind.CommRing.Mon.unit => h_1 ()
    | Lean.Grind.CommRing.Mon.mult p m => h_2 p m) =
    h_1 ()
-- Std.Http.Data.URI.Basic
Std.Http.RequestTarget.instEncodeV11 : Std.Http.Internal.Encode Std.Http.Version.v11 Std.Http.RequestTarget
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mker_fst : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.mker (MonoidHom.fst M N) = ⊥.prod ⊤
-- Lean.Parser.Attr
Lean.Parser.Attr.extern.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app_assoc : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) (A : ↑X) {Z : ↑Y} (h : F.toFunctor.obj A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.hom.toNatTrans.app A)
      (CategoryTheory.CategoryStruct.comp (e.inv.toNatTrans.app A) h) =
    h
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.id_app : ∀ {n : ℕ} (X : SSet.Truncated n) (d : (SimplexCategory.Truncated n)ᵒᵖ),
  (CategoryTheory.CategoryStruct.id X).app d = CategoryTheory.CategoryStruct.id (X.obj d)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prodFunctor_map : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {X Y : CategoryTheory.Functor A B × CategoryTheory.Functor C D}
  (nm : X ⟶ Y), CategoryTheory.prodFunctor.map nm = CategoryTheory.NatTrans.prod nm.1 nm.2
-- Mathlib.Topology.Homotopy.Equiv
/-- Any homeomorphism is a homotopy equivalence.
 -/
Homeomorph.toHomotopyEquiv : {X : Type u} →
  {Y : Type v} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → X ≃ₜ Y → ContinuousMap.HomotopyEquiv X Y
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
/-- A functor `N ⥤ (fiber p).Elements` which is initial when `N`
is cofiltered and initially small.  -/
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      {N : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} N] →
          (p : CategoryTheory.Functor N C) →
            [inst_3 : CategoryTheory.InitiallySmall N] →
              CategoryTheory.Functor N (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber p).Elements
-- Mathlib.Topology.Sheaves.Presheaf
IsOpenMap.pullbackIso_inv_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (X_1 : TopCat.Presheaf C Y)
  (X_2 : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (hf.pullbackIso.inv.app X_1).app X_2 = (TopCat.Presheaf.pullbackObjObjOfImageOpen f X_1 (Opposite.unop X_2) ⋯).inv
-- Mathlib.Order.Booleanisation
Booleanisation.instPreorder : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → Preorder (Booleanisation α)
-- Mathlib.RingTheory.SimpleModule.Isotypic
isIsotypic_iff_isFullyInvariant_imp_bot_or_top : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M],
  IsIsotypic R M ↔ ∀ (N : Submodule R M), N.IsFullyInvariant → N = ⊥ ∨ N = ⊤
-- Mathlib.Order.CompleteLattice.Basic
le_sInf_inter : ∀ {α : Type u_1} [inst : CompleteLattice α] {s t : Set α}, sInf s ⊔ sInf t ≤ sInf (s ∩ t)
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabShow : Lean.Elab.Term.TermElab
-- Mathlib.Logic.Basic
if_ctx_congr : ∀ {α : Sort u_1} {P Q : Prop} [inst : Decidable P] [inst_1 : Decidable Q] {x y u v : α},
  (P ↔ Q) → (Q → x = u) → (¬Q → y = v) → (if P then x else y) = if Q then u else v
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.lintegral_add : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (f g : α →ₘ[μ] ENNReal),
  (f + g).lintegral = f.lintegral + g.lintegral
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.isoMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (h h_1 : V₀.V ≅ V₁.V) (e_h : h = h_1)
  (w : CategoryTheory.CategoryStruct.comp V₀.str (F.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom V₁.str),
  CategoryTheory.Endofunctor.Coalgebra.isoMk h w = CategoryTheory.Endofunctor.Coalgebra.isoMk h_1 ⋯
-- Mathlib.Order.RelSeries
LTSeries.length_withLength : ∀ (α : Type u_1) [inst : Preorder α] [inst_1 : InfiniteDimensionalOrder α] (n : ℕ), (LTSeries.withLength α n).length = n
-- Mathlib.Algebra.Ring.Parity
Nat.odd_add' : ∀ {m n : ℕ}, Odd (m + n) ↔ (Odd n ↔ Even m)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.MulticospanIndex.multicospan.match_1.eq_1 : ∀ {J : CategoryTheory.Limits.MulticospanShape}
  (motive : (x y : CategoryTheory.Limits.WalkingMulticospan J) → (x ⟶ y) → Sort u_3)
  (x : CategoryTheory.Limits.WalkingMulticospan J)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingMulticospan J) → motive x x (CategoryTheory.Limits.WalkingMulticospan.Hom.id x))
  (h_2 :
    (b : J.R) →
      motive (CategoryTheory.Limits.WalkingMulticospan.left (J.fst b))
        (CategoryTheory.Limits.WalkingMulticospan.right b) (CategoryTheory.Limits.WalkingMulticospan.Hom.fst b))
  (h_3 :
    (b : J.R) →
      motive (CategoryTheory.Limits.WalkingMulticospan.left (J.snd b))
        (CategoryTheory.Limits.WalkingMulticospan.right b) (CategoryTheory.Limits.WalkingMulticospan.Hom.snd b)),
  (match x, x, CategoryTheory.Limits.WalkingMulticospan.Hom.id x with
    | x, .(x), CategoryTheory.Limits.WalkingMulticospan.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingMulticospan.left (J.fst b)), .(CategoryTheory.Limits.WalkingMulticospan.right b),
      CategoryTheory.Limits.WalkingMulticospan.Hom.fst b => h_2 b
    | .(CategoryTheory.Limits.WalkingMulticospan.left (J.snd b)), .(CategoryTheory.Limits.WalkingMulticospan.right b),
      CategoryTheory.Limits.WalkingMulticospan.Hom.snd b => h_3 b) =
    h_1 x
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.Equivalent.refl : ∀ {R : Type u_2} {M : Type u_4} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N), Q.Equivalent Q
-- Mathlib.Analysis.Complex.CanonicalDecomposition
Complex.canonicalFactor_apply : ∀ (R : ℝ) (w z : ℂ), Complex.canonicalFactor R w z = (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w))
-- Mathlib.Order.Bounds.Basic
IsLUB.nonempty : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α} [NoBotOrder α], IsLUB s a → s.Nonempty
-- Mathlib.Order.CompleteSublattice
/-- The pull back of a complete sublattice under a complete lattice hom is a complete sublattice.  -/
CompleteSublattice.comap : {α : Type u_1} →
  {β : Type u_2} →
    [inst : CompleteLattice α] →
      [inst_1 : CompleteLattice β] → CompleteLatticeHom α β → CompleteSublattice β → CompleteSublattice α
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.Tendsto.const_div : ∀ {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a b : ENNReal},
  Filter.Tendsto m f (nhds b) → b ≠ ⊤ ∨ a ≠ ⊤ → Filter.Tendsto (fun b => a / m b) f (nhds (a / b))
-- Mathlib.Data.Rel.Cover
SetRel.isCover_univ : ∀ {X : Type u_1} {s N : Set X}, SetRel.IsCover Set.univ s N ↔ s.Nonempty → N.Nonempty
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.divisionCommMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : Inv M₁]
  [inst_4 : Div M₁] [inst_5 : Pow M₁ ℤ] [inst_6 : DivisionCommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
  (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n),
  Function.Injective.divisionCommMonoid f hf one mul inv div npow zpow =
    { toDivisionMonoid := Function.Injective.divisionMonoid f hf one mul inv div npow zpow, mul_comm := ⋯ }
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {ι : C → Type w} {X : C}
  {R : CategoryTheory.Presieve X} (hR : R ∈ K.coverings X)
  (h : ⦃W : C⦄ → (r : W ⟶ X) → R r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W)
  (R_1 : CategoryTheory.Presieve X) (hR_1 : R_1 ∈ K.coverings X)
  (h_1 : ⦃W : C⦄ → (r : W ⟶ X) → R_1 r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W),
  (CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h =
      CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR_1 h_1) =
    (R = R_1 ∧ h ≍ h_1)
-- Mathlib.Order.Sublattice
Sublattice.coe_copy : ∀ {α : Type u_2} [inst : Lattice α] (L : Sublattice α) (s : Set α) (hs : s = ↑L), ↑(L.copy s hs) = s
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.codisjoint_range_inl_range_inr : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H],
  Codisjoint AddMonoid.Coprod.inl.range AddMonoid.Coprod.inr.range
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_eq_some_get!_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {a : α}, m.contains a = true → m.get? a = some (m.get! a)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) [commRingObj : CategoryTheory.CommRingObj X] (X_1 : C)
  (commRingObj_1 : CategoryTheory.CommRingObj X_1),
  ({ X := X, commRingObj := commRingObj } = { X := X_1, commRingObj := commRingObj_1 }) =
    (X = X_1 ∧ commRingObj ≍ commRingObj_1)
-- Mathlib.Topology.UniformSpace.Basic
AddOpposite.uniformContinuous_op : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous AddOpposite.op
-- Aesop.Tree.Data
Aesop.GoalData.id : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Aesop.GoalId
-- Mathlib.RingTheory.RingHom.FaithfullyFlat
RingHom.faithfullyFlat_algebraMap_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (algebraMap R S).FaithfullyFlat ↔ Module.FaithfullyFlat R S
-- Mathlib.Algebra.Ring.Defs
Semiring.toMonoid : {α : Type u} → [self : Semiring α] → Monoid α
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.self_comp_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N), ⇑e ∘ ⇑e.symm = id
-- Mathlib.Geometry.Euclidean.SignedDist
abs_signedDist_le_dist : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P), |((signedDist v) p) q| ≤ dist p q
-- Mathlib.FieldTheory.Cardinality
/-- A finite field has prime power cardinality.  -/
Fintype.isPrimePow_card_of_field : ∀ {α : Type u_1} [inst : Fintype α] [Field α], IsPrimePow (Fintype.card α)
-- Mathlib.Topology.AlexandrovDiscrete
alexandrovDiscrete_iff : ∀ (α : Type u_1) [inst : TopologicalSpace α],
  AlexandrovDiscrete α ↔ ∀ (S : Set (Set α)), (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S)
-- Init.Data.Nat.Basic
Nat.beq_eq_true_eq : ∀ (a b : ℕ), ((a == b) = true) = (a = b)