mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.equivCostructuredArrow_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  (CategoryTheory.Limits.Cone.equivCostructuredArrow F).unitIso =
    CategoryTheory.NatIso.ofComponents CategoryTheory.Limits.Cone.eta ⋯
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → ∀ {h : k' ∈ Std.HashMap.ofList l}, (Std.HashMap.ofList l)[k'] = v
-- Mathlib.Algebra.Group.Pointwise.Finset.Density
Finset.dens_neg : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : InvolutiveNeg α] [inst_2 : Fintype α] (s : Finset α),
  (-s).dens = s.dens
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- The conditions on a spectral object indexed by `EInt` which allow
to obtain a (convergent) third quadrant `E₂` cohomological spectral sequence,
or a (convergent) first quadrant `E₂` *homological* spectral sequence  -/
CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.Abelian.SpectralObject C EInt → Prop
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Helper type used during pattern normalization.
When normalizing a sub-pattern `p`, we store the kind of the parent pattern
using this enumeration type.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.ParentKind : Type
-- Mathlib.Data.List.Nodup
List.nodup_iff_injective_get : ∀ {α : Type u} {l : List α}, l.Nodup ↔ Function.Injective l.get
-- Init.Data.Int.DivMod.Lemmas
Int.add_bmod_eq_add_bmod_left : ∀ {x : ℤ} {n : ℕ} {y : ℤ} (i : ℤ), x.bmod n = y.bmod n → (i + x).bmod n = (i + y).bmod n
-- Mathlib.Data.Multiset.Fintype
Multiset.instIsEmptyToTypeOfNat : ∀ {α : Type u_1} [inst : DecidableEq α], IsEmpty (Multiset.ToType 0)
-- Mathlib.Data.Finmap
/-- The set of keys of a finite map.  -/
Finmap.keys : {α : Type u} → {β : α → Type v} → Finmap β → Finset α
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toLinearMap_mkL_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x : E),
  ↑((TensorProduct.mkL 𝕜 E F) x) = (TensorProduct.mk 𝕜 E F) x
-- Init.Data.Range.Polymorphic.NatLemmas
Std.PRange.Nat.succMany_eq : ∀ {m n : ℕ}, Std.PRange.succMany n m = m + n
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β] (f : sInfHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = f
-- Lean.DocString.Parser
Lean.Doc.Parser.metadataContents.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.ZMod.Coprime
/-- If an integer `a` and a prime `p` satisfy `gcd a p = 1`, then `a : ZMod p` is nonzero.  -/
ZMod.ne_zero_of_gcd_eq_one : ∀ {a : ℤ} {p : ℕ}, Nat.Prime p → a.gcd ↑p = 1 → ↑a ≠ 0
-- Mathlib.AlgebraicGeometry.Scheme
/-- The spectrum of a commutative ring, as a scheme.  -/
AlgebraicGeometry.Spec : CommRingCat → AlgebraicGeometry.Scheme
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.of_injective : ∀ (k : Type u_1) (G : Type u_2) [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k] [Nontrivial k],
  Function.Injective ⇑(SkewMonoidAlgebra.of k G)
-- Mathlib.Order.Filter.Cofinite
Set.Finite.eventually_cofinite_notMem : ∀ {α : Type u_2} {s : Set α}, s.Finite → ∀ᶠ (x : α) in Filter.cofinite, x ∉ s
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsIntTangentAt.isIntTangent : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P} {p : P},
  s₁.IsIntTangentAt s₂ p → s₁.IsIntTangent s₂
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.check : Array Lean.Elab.DefViewElabHeader → Lean.Elab.DefViewElabHeader → Lean.Elab.TermElabM Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.precomp_h : ∀ {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {C : Z.Subcomplex}
  {ψ : B.toSSet ⟶ C.toSSet} {f' g' : SSet.RelativeMorphism B C ψ} (h : f'.Homotopy g') (f : SSet.RelativeMorphism A B φ)
  {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ),
  (h.precomp f fac).h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.map (SSet.stdSimplex.obj { len := 1 })) h.h
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.IsParabolic.neg : ∀ {R : Type u_1} [inst : CommRing R] {m : Matrix (Fin 2) (Fin 2) R}, m.IsParabolic → (-m).IsParabolic
-- Std.Time.Format.Modifier
Std.Time.Modifier.H.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.H presentation = Std.Time.Modifier.H presentation_1 → presentation = presentation_1
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsCongr_inv_app : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] {f g : R →+* S} (e : f = g) (M : ModuleCat S) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.restrictScalarsCongr e).inv.app M)) x = x
-- Mathlib.Data.NNReal.Basic
NNReal.le_mul_iInf : ∀ {ι : Sort u_3} [Nonempty ι] {a g : NNReal} {h : ι → NNReal}, (∀ (j : ι), a ≤ g * h j) → a ≤ g * iInf h
-- Init.Data.Rat.Lemmas
Rat.le_antisymm_iff : ∀ {a b : ℚ}, a = b ↔ a ≤ b ∧ b ≤ a
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
/-- If a non-unital subalgebra of a non-unital topological algebra is commutative, then so is its
topological closure.

See note [reducible non-instances].  -/
NonUnitalSubalgebra.nonUnitalCommSemiringTopologicalClosure : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : Module R A] →
            [inst_4 : ContinuousConstSMul R A] →
              [inst_5 : IsSemitopologicalSemiring A] →
                [T2Space A] →
                  (s : NonUnitalSubalgebra R A) →
                    (∀ (x y : ↥s), x * y = y * x) → NonUnitalCommSemiring ↥s.topologicalClosure
-- Init.Data.Array.Mem
Array.sizeOf_lt_of_mem : ∀ {α : Type u_1} {a : α} [inst : SizeOf α] {as : Array α}, a ∈ as → sizeOf a < sizeOf as
-- Aesop.Builder.Basic
Aesop.RuleBuilderOptions.casesPatterns? : Aesop.RuleBuilderOptions → Option (Array Aesop.CasesPattern)
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
/-- If `G` has a cyclic Sylow `p`-subgroup, then the cardinality and index of the commutator
subgroup of `G` cannot both be divisible by `p`.  -/
Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite G] (P : Sylow p G) [IsCyclic ↥↑P],
  ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index
-- Mathlib.Algebra.Free
FreeSemigroup.instTraversable : Traversable FreeSemigroup
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.IsGeneratedBy.isFinite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (G : CategoryTheory.Subfunctor F) {ι : Type w'} [Finite ι] {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)},
  G.IsGeneratedBy x → G.IsFinite
-- Mathlib.Topology.Compactness.Lindelof
HereditarilyLindelofSpace.of_forall_isOpen : ∀ {X : Type u} [inst : TopologicalSpace X], (∀ (s : Set X), IsOpen s → IsLindelof s) → HereditarilyLindelofSpace X
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVLogicalExpr.sat_and : ∀ {x y : Std.Tactic.BVDecide.BVLogicalExpr} {assign : Std.Tactic.BVDecide.BVExpr.Assignment},
  x.Sat assign →
    y.Sat assign →
      Std.Tactic.BVDecide.BVLogicalExpr.Sat (Std.Tactic.BVDecide.BoolExpr.gate Std.Tactic.BVDecide.Gate.and x y) assign
-- Mathlib.Tactic.Variable
_private.Mathlib.Tactic.Variable.0.Mathlib.Command.Variable.elabVariables.extendScope : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Algebra.Algebra.Hom
AlgHom.mk.injEq : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (toRingHom : A →+* B)
  (commutes' : ∀ (r : R), (↑↑toRingHom).toFun ((algebraMap R A) r) = (algebraMap R B) r) (toRingHom_1 : A →+* B)
  (commutes'_1 : ∀ (r : R), (↑↑toRingHom_1).toFun ((algebraMap R A) r) = (algebraMap R B) r),
  ({ toRingHom := toRingHom, commutes' := commutes' } = { toRingHom := toRingHom_1, commutes' := commutes'_1 }) =
    (toRingHom = toRingHom_1)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RicSliceData : (α : Type u) → [Ord α] → Type u
-- Lean.Level
Lean.Level.PP.Result.imaxNode.injEq : ∀ (a a_1 : List Lean.Level.PP.Result), (Lean.Level.PP.Result.imaxNode a = Lean.Level.PP.Result.imaxNode a_1) = (a = a_1)
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.support_mul_subset_left : ∀ {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β] {g₁ g₂ : α →₀ β}, (g₁ * g₂).support ⊆ g₁.support
-- Batteries.Data.Fin.Fold
Fin.dfoldl_eq_dfoldlM : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} (f : (i : Fin n) → α i.castSucc → α i.succ) (x : α 0),
  Fin.dfoldl n α f x = Fin.dfoldlM n α f x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_mul_right' : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Group α] {t : Finset α} {b : α},
  Finset.image (fun x => x * b⁻¹) t = t.preimage (fun x => x * b) ⋯
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.measurableSet_fundamentalCone : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], MeasurableSet (NumberField.mixedEmbedding.fundamentalCone K)
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.coe_neg : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddGroup 𝕜] [inst_1 : LE α] (f : IncidenceAlgebra 𝕜 α), ⇑(-f) = -⇑f
-- Batteries.Data.Array.Match
Array.Matcher.mk.injEq : ∀ {α : Type u_1} (table : Array.PrefixTable α) (state : Fin (table.size + 1)) (table_1 : Array.PrefixTable α)
  (state_1 : Fin (table_1.size + 1)),
  ({ table := table, state := state } = { table := table_1, state := state_1 }) = (table = table_1 ∧ state ≍ state_1)
-- Mathlib.RingTheory.Localization.Submodule
IsFractionRing.coeSubmodule_strictMono : ∀ {R : Type u_3} {K : Type u_4} [inst : CommRing R] [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K],
  StrictMono (IsLocalization.coeSubmodule K)
-- Mathlib.RingTheory.QuasiFinite.Weakly
/-- Use `Algebra.QuasiFiniteAt.of_surjectiveOnStalks` instead for `Algebra.QuasiFiniteAt R p`.  -/
Algebra.WeaklyQuasiFiniteAt.of_surjectiveOnStalks : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T] (p : Ideal S) [inst_5 : p.IsPrime] [Algebra.WeaklyQuasiFiniteAt R p]
  (q : Ideal T) [inst_7 : q.IsPrime] (f : S →ₐ[R] T),
  f.SurjectiveOnStalks → p = Ideal.comap f q → Algebra.WeaklyQuasiFiniteAt R q
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Replacing a point in an affinely independent triple with another point on the same
line preserves affine independence.  -/
affineIndependent_iff_affineIndependent_collinear_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ p : P},
  Collinear k {p₂, p, p₃} → p₂ ≠ p → p₂ ≠ p₃ → (AffineIndependent k ![p₁, p₂, p] ↔ AffineIndependent k ![p₁, p₂, p₃])
-- Mathlib.Topology.Path
Path.truncate_one_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b), γ.truncate 1 1 = (Path.refl b).cast ⋯ ⋯
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.mem_map_iff_mem : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N},
  Function.Injective ⇑f → ∀ {K : AddSubgroup G} {x : G}, f x ∈ AddSubgroup.map f K ↔ x ∈ K
-- Mathlib.Order.Partition.Basic
Partition.iSup_eq : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] (P : Partition s), ⨆ x ∈ P, x = s
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_div_sup_mul_mabs_div_inf : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b c : α),
  |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.forget_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C), (CategoryTheory.AddMon.forget C).obj A = A.X
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.IsLimit.mk_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I)
  (lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt)
  (fac :
    ∀ (E : CategoryTheory.Limits.Multifork I) (i : J.L), CategoryTheory.CategoryStruct.comp (lift E) (K.ι i) = E.ι i)
  (uniq :
    ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt),
      (∀ (i : J.L), CategoryTheory.CategoryStruct.comp m (K.ι i) = E.ι i) → m = lift E)
  (E : CategoryTheory.Limits.Multifork I), (CategoryTheory.Limits.Multifork.IsLimit.mk K lift fac uniq).lift E = lift E
-- Mathlib.GroupTheory.Order.Min
ZMod.minOrder_of_prime : ∀ {p : ℕ}, Nat.Prime p → AddMonoid.minOrder (ZMod p) = ↑p
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.reindex_mulEquiv : ∀ {B : Type u_1} {B' : Type u_2} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W)
  (e : B ≃ B'), (cs.reindex e).mulEquiv = cs.mulEquiv.trans (M.reindexGroupEquiv e).symm
-- Mathlib.Analysis.Normed.Group.Bounded
/-- A helper lemma used to prove that the (scalar or usual) product of a function that tends to one
and a bounded function tends to one. This lemma is formulated for any binary operation
`op : E → F → G` with an estimate `‖op x y‖ ≤ ‖x‖ * ‖y‖` instead of multiplication so that it
can be applied to `(*)`, `flip (*)`, `(•)`, and `flip (•)`.  -/
Filter.Tendsto.op_one_isBoundedUnder_le : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : SeminormedGroup G] {f : α → E} {g : α → F} {l : Filter α},
  Filter.Tendsto f l (nhds 1) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ g) →
      ∀ (op : E → F → G),
        (∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖) → Filter.Tendsto (fun x => op (f x) (g x)) l (nhds 1)
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_norm_expr : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.norm_eq_cert lhs rhs p = true →
    Int.Internal.Linear.Expr.denote ctx lhs = Int.Internal.Linear.Expr.denote ctx rhs →
      Int.Internal.Linear.Poly.denote' ctx p = 0
-- Std.Tactic.BVDecide.Syntax
Lean.Elab.Tactic.BVDecide.SolverMode.proof.sizeOf_spec : sizeOf Lean.Elab.Tactic.BVDecide.SolverMode.proof = 1
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicator_mono : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ₁ δ₂ : ℝ} (δ₁_pos : 0 < δ₁) (δ₂_pos : 0 < δ₂),
  δ₁ ≤ δ₂ → ∀ (E : Set α), ⇑(thickenedIndicator δ₁_pos E) ≤ ⇑(thickenedIndicator δ₂_pos E)
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.cancel_factors_le : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b ad bd a' b' gcd : α},
  ad * a = a' → bd * b = b' → 0 < ad → 0 < bd → 0 < gcd → (a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_toList : ∀ {M : Type u_7} [inst : CommMonoid M] (s : Finset M), s.toList.prod = ∏ x ∈ s, x
-- Mathlib.NumberTheory.ModularForms.NormTrace
ModularForm.isZero_of_neg_weight : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] {k : ℤ}, k < 0 → ∀ (f : ModularForm 𝒢 k), f = 0
-- Mathlib.NumberTheory.LegendreSymbol.Basic
legendreSym.at_zero : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], legendreSym p 0 = 0
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPInstanceTypes : Lean.Options → Bool
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.inl_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.kernelCokernelCompSequence.φ f g) =
    CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.inl
-- Mathlib.Logic.Function.FiberPartition
Function.Fiber.map_preimage_eq_image : ∀ {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (a : Function.Fiber f),
  f (Function.Fiber.preimage f a) = Function.Fiber.image f a
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.exact₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Z : C}
  (I : CategoryTheory.InjectiveResolution Z),
  { X₁ := ((CochainComplex.single₀ C).obj Z).X 0, X₂ := I.cocomplex.X 0, X₃ := I.cocomplex.X 1, f := I.ι.f 0,
      g := I.cocomplex.d 0 1, zero := ⋯ }.Exact
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.strictMono_y : ∀ {a : ℕ} (a1 : 1 < a), StrictMono (Pell.yn a1)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- A left homology data `h` of a short complex `S` is preserved by a functor `F` is
`F` preserves the kernel of `S.g : S.X₂ ⟶ S.X₃` and the cokernel of `h.f' : S.X₁ ⟶ h.K`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy : {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.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {S : CategoryTheory.ShortComplex C} →
              S.LeftHomologyData → (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → Prop
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.fac : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCartesian f φ]
  {R' : 𝒮} {a' : 𝒳} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryTheory.CategoryStruct.comp g f) (φ' : a' ⟶ b)
  [inst_3 : p.IsHomLift f' φ'],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f φ hf' φ') φ = φ'
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_indep_eq : ∀ {α : Type u_1} {M : Matroid α}, M.removeLoops.Indep = M.Indep
-- Lean.Elab.Match
Lean.Elab.Term.TermMatchAltView : Type
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_hom_app_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Precoherent C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).counitIso.hom.app X).hom.app X_1 =
    X.obj.map (e.counitIso.inv.app (Opposite.unop X_1)).op
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.measurableSet_injective : ∀ {α : Type u_1}, Function.Injective (@MeasurableSet α)
-- Mathlib.RingTheory.Algebraic.Basic
Transcendental.uniqueFactorizationMonoid_adjoin : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S]
  [UniqueFactorizationMonoid R] {s : S}, Transcendental R s → UniqueFactorizationMonoid ↥R[s]
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.im_ofNat : ∀ {R : Type u_1} {a b : R} [inst : AddCommMonoidWithOne R] (n : ℕ) [inst_1 : n.AtLeastTwo], (OfNat.ofNat n).im = 0
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff : ∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  (E : CategoryTheory.PreZeroHypercover X),
  E.presieve₀ ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings X ↔
    (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑(E.f i)) ∧ ∀ (i : E.I₀), P (E.f i)
-- Mathlib.Computability.DFA
DFA.comap_start : ∀ {α : Type u} {σ : Type v} {α' : Type u_1} (f : α' → α) (M : DFA α σ), (DFA.comap f M).start = M.start
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.eq_of_eqOn_dense : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {s : Set M},
  (FirstOrder.Language.Substructure.closure L).toFun s = ⊤ → ∀ {f g : L.Hom M N}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [BEq α] [inst_3 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {km : α}, Std.Internal.List.minKey? l = some km → Std.Internal.List.getKey? km l = some km
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.inv_image_trans_target : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z),
  ↑e'.symm '' (e.trans e').target = e'.source ∩ e.target
-- Mathlib.Algebra.Ring.GeomSum
neg_one_geom_sum : ∀ {R : Type u_1} [inst : Ring R] {n : ℕ}, ∑ i ∈ Finset.range n, (-1) ^ i = if Even n then 0 else 1
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxKeyD.match_1.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) (size : ℕ) (k : α)
  (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
  (l_1 r : Std.DTreeMap.Internal.Impl α β) (fallback : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_2 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1 →
                      (fallback : α) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r),
      fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1),
      fallback => h_3 size k v l r size_2 k_2 v_2 l_2 r_1 h fallback) =
    h_3 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯ fallback
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
/-- The derivative of `polarCoord.symm`, see `hasFDerivAt_polarCoord_symm`.  -/
fderivPolarCoordSymm : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ