mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.equation_negAdd : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Equation x₁ y₁ →
    W.Equation x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        W.Equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.φ_monic : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, E ≠ ⊥ → (RatFunc.Luroth.φ✝ E).Monic
-- Mathlib.Tactic.Abel
/-- `abel` solves equations in the language of *additive*, commutative monoids and groups.

`abel` and its variants work as both tactics and conv tactics.

* `abel1` fails if the target is not an equality that is provable by the axioms of
  commutative monoids/groups.
* `abel_nf` rewrites all group expressions into a normal form.
  * `abel_nf at h` rewrites in a hypothesis.
  * `abel_nf (config := cfg)` allows for additional configuration:
    * `red`: the reducibility setting (overridden by `!`).
    * `zetaDelta`: if true, local `let` variables can be unfolded (overridden by `!`).
    * `recursive`: if true, `abel_nf` also recurses into atoms.
* `abel!`, `abel1!`, `abel_nf!` use a more aggressive reducibility setting to identify atoms.

Examples:
```
example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
```
 -/
Mathlib.Tactic.Abel.tacticAbel_nf!__ : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α}
  {v : β},
  t.WF →
    (Std.DTreeMap.Internal.Impl.Const.get? t k = some v ↔
      ∃ k', compare k k' = Ordering.eq ∧ (k', v) ∈ Std.DTreeMap.Internal.Impl.Const.toList t)
-- Init.Data.Nat.Lemmas
Nat.add_add_add_comm : ∀ (a b c d : ℕ), a + b + (c + d) = a + c + (b + d)
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_lineMap_left : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  nndist ((AffineMap.lineMap p₁ p₂) c) p₁ = ‖c‖₊ * nndist p₁ p₂
-- Mathlib.LinearAlgebra.Dual.Defs
LinearEquiv.dualMap_refl : ∀ {R : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁],
  (LinearEquiv.refl R M₁).dualMap = LinearEquiv.refl R (Module.Dual R M₁)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.mk.sizeOf_spec : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} (inv : SSet.Edge x₁ x₀)
  (homInvId : hom.CompStruct inv (SSet.Edge.id x₀)) (invHomId : inv.CompStruct hom (SSet.Edge.id x₁)),
  sizeOf { inv := inv, homInvId := homInvId, invHomId := invHomId } = 1 + sizeOf inv + sizeOf homInvId + sizeOf invHomId
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- The group homomorphism from `CongruenceSubgroup.Gamma0` to `ZMod N` given by
mapping a matrix to its lower right-hand entry.  -/
CongruenceSubgroup.Gamma0Map : (N : ℕ) → ↥(CongruenceSubgroup.Gamma0 N) →* ZMod N
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
NonarchimedeanGroup.toIsTopologicalGroup : ∀ {G : Type u_1} {inst : Group G} {inst_1 : TopologicalSpace G} [self : NonarchimedeanGroup G], IsTopologicalGroup G
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
/-- The single object covering by one surjective morphism satisfying `P`.  -/
AlgebraicGeometry.Scheme.Hom.cover : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X S : AlgebraicGeometry.Scheme} →
    (f : X ⟶ S) →
      P f → [AlgebraicGeometry.Surjective f] → AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S
-- Lean.Data.Position
Lean.Position.mk.injEq : ∀ (line column line_1 column_1 : ℕ),
  ({ line := line, column := column } = { line := line_1, column := column_1 }) = (line = line_1 ∧ column = column_1)
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- Typecheck a `BialgHom` as a morphism in `CommHopfAlgCat R`.  -/
CommHopfAlgCat.ofHom : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      {x : CommRing X} →
        {x_1 : CommRing Y} →
          {x_2 : HopfAlgebra R X} →
            {x_3 : HopfAlgebra R Y} →
              (X →ₐc[R] Y) →
                ({ X := X, commRing := x, hopfAlgebra := x_2 } ⟶ { X := Y, commRing := x_1, hopfAlgebra := x_3 })
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isMatch_iff_exists_splits : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch pat pos ↔
    ∃ t₁ t₂, pos.Splits t₁ t₂ ∧ String.Slice.Pattern.Model.PatternModel.Matches pat t₁
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.DefEqCacheKey.mk : Lean.Expr → Lean.Expr → UInt64 → Lean.Meta.DefEqCacheKey
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filterMap_eq_filterMap! : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced}
  {f : (a : α) → β a → Option (γ a)},
  (Std.DTreeMap.Internal.Impl.filterMap f t h).impl = Std.DTreeMap.Internal.Impl.filterMap! f t
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- This is not an instance to avoid type class inference loops. See
`WeakDual.Complex.instStarHomClass`.  -/
AlgHomClass.instStarHomClass : ∀ {F : Type u_1} {A : Type u_2} [inst : CStarAlgebra A] [inst_1 : FunLike F A ℂ] [hF : AlgHomClass F ℂ A ℂ],
  StarHomClass F A ℂ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.contains_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, m₁.Equiv m₂ → m₁.contains k = m₂.contains k
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Matrix.charpoly.univ_coeff_isHomogeneous : ∀ (R : Type u_1) (n : Type u_3) [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (i j : ℕ),
  i + j = Fintype.card n → ((Matrix.charpoly.univ R n).coeff i).IsHomogeneous j
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.instMul : {R : Type u} → [inst : CommRing R] → Mul (WeierstrassCurve.VariableChange R)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.merge_aux : ∀ {α : Type u_1} [inst : Preorder α] {l r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l o₂ →
    Ordnode.Valid' o₁ r o₂ →
      Ordnode.All (fun x => Ordnode.All (fun y => x < y) r) l →
        Ordnode.Valid' o₁ (l.merge r) o₂ ∧ (l.merge r).size = l.size + r.size
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.Hom.mk.sizeOf_spec : ∀ {M N : SemiNormedGrp} (hom' : NormedAddGroupHom M.carrier N.carrier), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.uniformContinuous : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → UniformContinuous f
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.deriv_negMulLog : ∀ {x : ℝ}, x ≠ 0 → deriv Real.negMulLog x = -Real.log x - 1
-- Lean.Meta.Match.SolveOverlap
/-- Solves the overlap assumptions expected by the alternative of a splitter
 -/
Lean.Meta.Match.solveOverlap : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_obj_snd : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (x : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).obj x).snd =
    S.snd.obj x
-- Mathlib.Topology.EMetricSpace.Defs
WeakPseudoEMetricSpace.ext : ∀ {α : Type u_2} [inst : TopologicalSpace α] {m m' : WeakPseudoEMetricSpace α}, m.toEDist = m'.toEDist → m = m'
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Congr!.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Congr!.Config
-- Mathlib.Algebra.Field.Defs
/-- `a ^ 0 = 1`  -/
DivisionSemiring.zpow_zero' : ∀ {K : Type u_2} [self : DivisionSemiring K] (a : K), a ^ 0 = 1
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.subtypeDomain_finsupp_sum : ∀ {γ : Type w} {ι : Type u_1} {β : ι → Type v} {δ : γ → Type x} [inst : DecidableEq γ] [inst_1 : (c : γ) → Zero (δ c)]
  [inst_2 : (c : γ) → (x : δ c) → Decidable (x ≠ 0)] [inst_3 : (i : ι) → AddCommMonoid (β i)] {p : ι → Prop}
  [inst_4 : DecidablePred p] {s : Π₀ (c : γ), δ c} {h : (c : γ) → δ c → Π₀ (i : ι), β i},
  DFinsupp.subtypeDomain p (s.sum h) = s.sum fun c d => DFinsupp.subtypeDomain p (h c d)
-- Mathlib.Data.Int.ModEq
Int.modEq_natAbs : ∀ {n a b : ℤ}, a ≡ b [ZMOD ↑n.natAbs] ↔ a ≡ b [ZMOD n]
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_smul_measure : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (c : ENNReal),
  ProbabilityTheory.mgf X (c • μ) t = c.toReal * ProbabilityTheory.mgf X μ t
-- Mathlib.Algebra.Star.Pointwise
Set.mem_star : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : Star α], a ∈ star s ↔ star a ∈ s
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.HasColimit.instHasColimit : ∀ {R : Type w} [inst : Ring R] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  (F : CategoryTheory.Functor J (ModuleCat R))
  [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))],
  CategoryTheory.Limits.HasColimit F
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_div_eq_nnnorm_right : ∀ {E : Type u_5} [inst : SeminormedGroup E] {x : E} (y : E), ‖x‖₊ = 0 → ‖x / y‖₊ = ‖y‖₊
-- Mathlib.Order.Filter.Map
Filter.map_comap_le : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β}, Filter.map m (Filter.comap m g) ≤ g
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.one_div_ne_zero : ∀ {p q r : NNReal}, p.HolderTriple q r → 1 / p ≠ 0
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.mem_sup_right : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {S T : NonUnitalStarSubalgebra R A} {x : A}, x ∈ T → x ∈ S ⊔ T
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
le_max_of_two_nsmul_le_add : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M] {a b c : M},
  2 • a ≤ b + c → a ≤ max b c
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.d : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → (self : HomologicalComplex V c) → (i j : ι) → self.X i ⟶ self.X j
-- Mathlib.Topology.Compactness.Compact
Prod.noncompactSpace_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  NoncompactSpace (X × Y) ↔ NoncompactSpace X ∧ Nonempty Y ∨ Nonempty X ∧ NoncompactSpace Y
-- Mathlib.Analysis.InnerProductSpace.Reproducing
_private.Mathlib.Analysis.InnerProductSpace.Reproducing.0.RKHS.kerFun.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (x : X),
  RKHS.kerFun H x = ContinuousLinearMap.adjoint (ContinuousLinearMap.proj x ∘SL RKHS.coeCLM 𝕜)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_eq_right : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ b → a ≤ b → a + b = b
-- Mathlib.Analysis.Convex.Quasiconvex
QuasiconvexOn.dual : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LE β] [inst_4 : SMul 𝕜 E] {s : Set E} {f : E → β},
  QuasiconvexOn 𝕜 s f → QuasiconcaveOn 𝕜 s (⇑OrderDual.toDual ∘ f)
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Debug `grind` by identifying places where it does not yet supersede `linarith`.  -/
linter.tacticAnalysis.regressions.linarithToGrind : Lean.Option Bool
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `iteratedFDeriv_sub_apply`

---

The iterated derivative of the difference of two functions is the difference of the iterated
derivatives.
 -/
fun_iteratedFDeriv_sub_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} {i : ℕ}
  {f g : E → F},
  ContDiffAt 𝕜 (↑i) f x →
    ContDiffAt 𝕜 (↑i) g x → iteratedFDeriv 𝕜 i (fun i => f i - g i) x = iteratedFDeriv 𝕜 i f x - iteratedFDeriv 𝕜 i g x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ENode.isRoot : Lean.Meta.Grind.ENode → Bool
-- Mathlib.Order.BooleanAlgebra.Basic
isCompl_compl : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], IsCompl x xᶜ
-- Mathlib.Algebra.Group.Submonoid.Finsupp
AddSubmonoid.mem_closure_range_iff_of_fintype : ∀ {M : Type u_1} [inst : AddCommMonoid M] {ι : Type u_2} {f : ι → M} {x : M} [inst_1 : Fintype ι],
  x ∈ AddSubmonoid.closure (Set.range f) ↔ ∃ a, x = ∑ i, a i • f i
-- Mathlib.FieldTheory.Finite.Basic
/-- **Fermat's Little Theorem**: for all nonzero `a : ZMod p`, we have `a ^ (p - 1) = 1`.  -/
ZMod.pow_card_sub_one_eq_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {a : ZMod p}, a ≠ 0 → a ^ (p - 1) = 1
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.memLp_two_iff_integrable_sq_norm : ∀ {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  {f : α → F},
  MeasureTheory.AEStronglyMeasurable f μ → (MeasureTheory.MemLp f 2 μ ↔ MeasureTheory.Integrable (fun x => ‖f x‖ ^ 2) μ)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.isMulCommutative_adjoin_singleton : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
  IsMulCommutative ↥R[x]
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.le_measure_sdiff`. -/
MeasureTheory.le_measure_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α}, μ s₁ - μ s₂ ≤ μ (s₁ \ s₂)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.toCyclesNatTrans_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.toCyclesNatTrans C).app S = S.toCycles
-- Std.Data.TreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
greater than the given key.
 -/
Std.TreeMap.getEntryGT : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.TreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.gt) → α × β
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.instMonoToRange : ∀ {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.Mono (SSet.Subcomplex.toRange f)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.injOn : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Nontrivial R], LinearIndepOn R v s → Set.InjOn v s
-- Init.Data.List.Scan.Lemmas
List.scanlM_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_3} {init : α} {x : β} {xs : List β} [inst : Monad m]
  [LawfulMonad m] {f : α → β → m α},
  List.scanlM f init (x :: xs) = do
    let __do_lift ← f init x
    let __do_lift ← List.scanlM f __do_lift xs
    pure (init :: __do_lift)
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.comp₂_iso_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} {x y z : a ⟶ b}
  {f : x ⟶ y} {g : y ⟶ z},
  (CategoryTheory.CategoryStruct.comp f g).iso.hom = CategoryTheory.CategoryStruct.comp f.iso.hom g.iso.hom
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.ofTop_apply : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {s₁ : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s₁] (h : s₁ = ⊤) (x : ↥s₁), (AffineIsometryEquiv.ofTop s₁ h) x = ↑x
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseRightKanExtension F L]
  [inst_5 : L.HasPointwiseRightKanExtension F],
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom)
      (L.pointwiseRightKanExtensionCounit (F.comp G)) =
    CategoryTheory.CategoryStruct.comp (L.associator (L.pointwiseRightKanExtension F) G).inv
      (CategoryTheory.Functor.whiskerRight (L.pointwiseRightKanExtensionCounit F) G)
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.ext : ∀ {K : Type u_1} {V : Type u_2} {inst : DivisionRing K} {inst_1 : AddCommGroup V} {inst_2 : Module K V}
  {x y : Projectivization.Subspace K V}, x.carrier = y.carrier → x = y
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.cancelBaseChangeAlg.eq_1 : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_8)
  (B : Type u_9) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (C : Type u_11) [inst_12 : CommRing C] [inst_13 : Algebra R C]
  [inst_14 : Algebra A C] [inst_15 : IsScalarTower R A C],
  Algebra.IsPushout.cancelBaseChangeAlg R S A B C =
    (AlgEquiv.ofLinearEquiv (Algebra.IsPushout.cancelBaseChange R S A B C).symm ⋯ ⋯).symm
-- Mathlib.Topology.Order.LeftRightNhds
/-- The following statements are equivalent:

0. `s` is a neighborhood of `b` within `(-∞, b)`
1. `s` is a neighborhood of `b` within `[a, b)`
2. `s` is a neighborhood of `b` within `(a, b)`
3. `s` includes `(l, b)` for some `l ∈ [a, b)`
4. `s` includes `(l, b)` for some `l < b`  -/
TFAE_mem_nhdsLT : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a b : α},
  a < b →
    ∀ (s : Set α),
      [s ∈ nhdsWithin b (Set.Iio b), s ∈ nhdsWithin b (Set.Ico a b), s ∈ nhdsWithin b (Set.Ioo a b),
          ∃ l ∈ Set.Ico a b, Set.Ioo l b ⊆ s, ∃ l ∈ Set.Iio b, Set.Ioo l b ⊆ s].TFAE
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.coe_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  (K : TopologicalSpace.NonemptyCompacts α) (L : TopologicalSpace.NonemptyCompacts β), ↑(K ×ˢ L) = ↑K ×ˢ ↑L
-- Mathlib.Data.Rat.Defs
Rat.mk_denom_ne_zero_of_ne_zero : ∀ {q : ℚ} {n d : ℤ}, q ≠ 0 → q = Rat.divInt n d → d ≠ 0
-- Batteries.Tactic.Alias
/-- The docstring for an alias.  -/
Batteries.Tactic.Alias.AliasInfo.toString : Batteries.Tactic.Alias.AliasInfo → String
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.commRingNorm.inj : ∀ {c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr} {e : Lean.Meta.Grind.Arith.CommRing.RingExpr}
  {p : Lean.Grind.CommRing.Poly} {c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr}
  {e_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr} {p_1 : Lean.Grind.CommRing.Poly},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.commRingNorm c e p =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.commRingNorm c_1 e_1 p_1 →
    c = c_1 ∧ e = e_1 ∧ p = p_1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_eq_if : ∀ {m n : ℕ}, (m<...=n).toArray = if m + 1 ≤ n then #[m + 1] ++ ((m + 1)<...=n).toArray else #[]
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- `ι : H ⟶ Q` is a kernel of `S.g' : Q ⟶ S.X₃`  -/
CategoryTheory.ShortComplex.RightHomologyData.hι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (self : S.RightHomologyData) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι self.ι ⋯)
-- Mathlib.RingTheory.OreLocalization.NonZeroDivisors
OreLocalization.instCommGroupWithZeroNonZeroDivisors : {R : Type u_1} →
  [inst : CommMonoidWithZero R] →
    [Nontrivial R] →
      [inst_2 : OreLocalization.OreSet (nonZeroDivisors R)] →
        [NoZeroDivisors R] → CommGroupWithZero (OreLocalization (nonZeroDivisors R) R)
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_ofBitVec : ∀ {b : BitVec 16}, { toBitVec := b }.toUInt64 = { toBitVec := BitVec.setWidth 64 b }
-- Mathlib.Topology.SeparatedMap
/-- If `p` is a locally injective separated map, and `A` is a connected space,
then two lifts `g₁, g₂ : A → E` of a map `f : A → X` are equal if they agree at one point.  -/
IsSeparatedMap.eq_of_comp_eq : ∀ {X : Type u_1} {E : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace A] {p : E → X}
  {g₁ g₂ : A → E},
  IsSeparatedMap p →
    IsLocallyInjective p →
      ∀ [PreconnectedSpace A], Continuous g₁ → Continuous g₂ → p ∘ g₁ = p ∘ g₂ → ∀ (a : A), g₁ a = g₂ a → g₁ = g₂
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toList_eq_match : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] [inst_3 : Std.PRange.LawfulUpwardEnumerable α],
  r.toList =
    match Std.PRange.succ? r.lower with
    | none => []
    | some next => next :: next<...*.toList
-- Mathlib.Algebra.CharP.Defs
ringExpChar.eq : ∀ (R : Type u_1) [inst : NonAssocSemiring R] (q : ℕ) [h : ExpChar R q], ringExpChar R = q
-- Init.Data.BitVec.Lemmas
BitVec.msb_eq_getLsbD_last : ∀ {w : ℕ} (x : BitVec w), x.msb = x.getLsbD (w - 1)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- a morphism between the first lines  -/
CategoryTheory.ShortComplex.SnakeInput.Hom.f₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} → S₁.Hom S₂ → (S₁.L₁ ⟶ S₂.L₁)
-- Init.Data.UInt.Lemmas
USize.le_of_lt : ∀ {a b : USize}, a < b → a ≤ b
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.head.match_1.splitter : {α : Type u_1} →
  (motive : (x : List α) → x ≠ [] → Sort u_2) →
    (x : List α) →
      (x_1 : x ≠ []) → ((a : α) → (tail : List α) → (x : a :: tail ≠ []) → motive (a :: tail) x) → motive x x_1
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.toUpper_inj : ∀ {α : Type u_1} {a b : α}, Topology.WithUpper.toUpper a = Topology.WithUpper.toUpper b ↔ a = b
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.isAffineOpen_top : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X], AlgebraicGeometry.IsAffineOpen ⊤