mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the second vector passed to `oangle` is 0, the result is 0.  -/
Orientation.oangle_zero_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V), o.oangle x 0 = 0
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Submodule.rank_le_one_iff_isPrincipal : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  (W : Submodule K V) [Module.Free K ↥W], Module.rank K ↥W ≤ 1 ↔ W.IsPrincipal
-- Aesop.EMap
Aesop.EMap.findWithKey? : {α : Type} → Lean.Expr → Aesop.EMap α → Lean.MetaM (Option (Lean.Expr × α))
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Construct an `AddMonoidHom` from `(⨂[R] i, s i)` to some space `F` from a function
`φ : (R × Π i, s i) → F` with the appropriate properties.  -/
PiTensorProduct.liftAddHom : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            {F : Type u_10} →
              [inst_3 : AddCommMonoid F] →
                (φ : R × ((i : ι) → s i) → F) →
                  (∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0) →
                    (∀ (f : (i : ι) → s i), φ (0, f) = 0) →
                      (∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
                          φ (r, Function.update f i m₁) + φ (r, Function.update f i m₂) =
                            φ (r, Function.update f i (m₁ + m₂))) →
                        (∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)) →
                          (∀ [inst_4 : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R),
                              φ (r, Function.update f i (r' • f i)) = φ (r' * r, f)) →
                            (PiTensorProduct R fun i => s i) →+ F
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
SemiNormedGrp.completion.map_normNoninc : ∀ {V W : SemiNormedGrp} {f : V ⟶ W},
  (SemiNormedGrp.Hom.hom f).NormNoninc → (SemiNormedGrp.Hom.hom (SemiNormedGrp.completion.map f)).NormNoninc
-- Init.Data.Nat.Basic
Nat.le_total : ∀ (m n : ℕ), m ≤ n ∨ n ≤ m
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsLocalMin.hasLineDerivAt_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {f : E → ℝ} {a b : E} {f' : ℝ}, IsLocalMin f a → HasLineDerivAt ℝ f f' a b → f' = 0
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.notMem_nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {x : ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl},
  x ∉ Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.AlgebraicGeometry.Limits
TopCat.Sheaf.isProductOfDisjoint.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Sheaf C X)
  (U V : TopologicalSpace.Opens ↑X) (h : U ⊓ V = ⊥), F.isProductOfDisjoint U V h = F.isProductOfDisjoint U V h
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t t_1 : Std.DTreeMap α β cmp) (e_t : t = t_1)
  (h : t.isEmpty = false), t.minKey h = t_1.minKey ⋯
-- Init.Data.Vector.Lemmas
Vector.toArray_eq_empty_iff : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.toArray = #[] ↔ n = 0
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_Ico : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] (a b : R),
  f.measure (Set.Ico a b) = ENNReal.ofReal (Function.leftLim (↑f) b - Function.leftLim (↑f) a)
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.whiskerLeft_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C)
  [inst_2 : CategoryTheory.MonoidalCoherence Y Z],
  CategoryTheory.MonoidalCoherence.iso =
    CategoryTheory.MonoidalCategory.whiskerLeftIso X CategoryTheory.MonoidalCoherence.iso
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_nonneg_of_ae_restrict : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b → 0 ≤ᵐ[μ.restrict (Set.Icc a b)] f → 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.pow_length_le_mul_ofDigits : ∀ {b : ℕ} {l : List ℕ} (hl : l ≠ []), l.getLast hl ≠ 0 → (b + 2) ^ l.length ≤ (b + 2) * Nat.ofDigits (b + 2) l
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.instMonoidalCategoryStruct : CategoryTheory.MonoidalCategoryStruct AugmentedSimplexCategory
-- Init.Data.UInt.Lemmas
UInt16.ofNat_bitVecToNat : ∀ (n : BitVec 16), UInt16.ofNat n.toNat = { toBitVec := n }
-- Mathlib.FieldTheory.RatFunc.Luroth
RatFunc.Luroth.transcendental_generator : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → Transcendental K (RatFunc.Luroth.generator E)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → k ∉ t₁ \ t₂
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
_private.Mathlib.CategoryTheory.Localization.Monoidal.Basic.0.CategoryTheory.Localization.Monoidal.termL' : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The forgetful functor from the category of ring objects in `C`
to the category of additive monoid objects in `C`.  -/
CategoryTheory.RingObjCat.forget₂AddMon : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.RingObjCat C) (CategoryTheory.AddMon C)
-- Mathlib.Algebra.Order.Field.Basic
/-- **Alias** of the reverse direction of `half_le_self_iff`. -/
half_le_self : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  0 ≤ a → a / 2 ≤ a
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Real.iter_deriv_exp : ∀ (n : ℕ), deriv^[n] Real.exp = Real.exp
-- Mathlib.Algebra.Order.Star.Conjneg
conjneg_nonpos : ∀ {G : Type u_1} {R : Type u_2} [inst : AddGroup G] [inst_1 : CommRing R] [inst_2 : PartialOrder R]
  [inst_3 : StarRing R] [StarOrderedRing R] {f : G → R}, conjneg f ≤ 0 ↔ f ≤ 0
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `mul_lt_mul_of_le_of_lt_of_pos_of_nonneg`. -/
mul_lt_mul_of_pos_of_nonneg : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulStrictMono α]
  [MulPosMono α], a ≤ b → c < d → 0 < a → 0 ≤ d → a * c < b * d
-- Mathlib.Algebra.Algebra.Basic
Algebra.algebraMap_ofSubsemiring_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {C : Type u_4} [inst_1 : SetLike C R] [inst_2 : SubsemiringClass C R] (S : C)
  (x : ↥S), (algebraMap (↥S) R) x = ↑x
-- Mathlib.Algebra.Ring.Equiv
/-- The two paths coercion can take to a `MonoidHom` are equivalent  -/
RingEquiv.toMonoidHom_commutes : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S),
  ↑↑f = (↑f).toMonoidHom
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_single : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} [inst : Fintype n] [inst_1 : DecidableEq n]
  [inst_2 : NonUnitalNonAssocSemiring R] (M : Matrix m n R) (j : n) (x : R),
  M.mulVec (Pi.single j x) = MulOpposite.op x • M.col j
-- Mathlib.Algebra.Group.Defs
nsmulRec.eq_2 : ∀ {M : Type u_1} [inst : Zero M] [inst_1 : Add M] (x : M) (n : ℕ), nsmulRec n.succ x = nsmulRec n x + x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.IsCycle.neighborSet_toSubgraph_internal : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {i : ℕ} {p : G.Walk u u},
  p.IsCycle → i ≠ 0 → i < p.length → p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isClosed_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set X},
  IsClosed (⇑h '' s) ↔ IsClosed s
-- Mathlib.Analysis.Calculus.Taylor
/-- **Taylor's theorem** as a limit.  -/
Real.taylor_tendsto : ∀ {f : ℝ → ℝ} {x₀ : ℝ} {n : ℕ} {s : Set ℝ},
  Convex ℝ s →
    x₀ ∈ s →
      ContDiffOn ℝ (↑n) f s →
        Filter.Tendsto (fun x => (f x - taylorWithinEval f n s x₀ x) / (x - x₀) ^ n) (nhdsWithin x₀ s) (nhds 0)
-- Mathlib.Order.Lattice
ofDual_max : ∀ {α : Type u} [inst : LinearOrder α] (a b : αᵒᵈ),
  OrderDual.ofDual (max a b) = min (OrderDual.ofDual a) (OrderDual.ofDual b)
-- Mathlib.Algebra.Homology.Embedding.Connect
/-- Given `h : ConnectData K L` and `n : ℕ` non-zero, the homology
of `h.cochainComplex` in degree `n` identifies to the homology of `L` in degree `n`.  -/
CochainComplex.ConnectData.homologyIsoPos : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : ChainComplex C ℕ} →
        {L : CochainComplex C ℕ} →
          (h : CochainComplex.ConnectData K L) →
            (n : ℕ) →
              [NeZero n] →
                (m : ℤ) →
                  m = ↑n →
                    [inst_3 : HomologicalComplex.HasHomology h.cochainComplex m] →
                      [inst_4 : HomologicalComplex.HasHomology L n] →
                        HomologicalComplex.homology h.cochainComplex m ≅ HomologicalComplex.homology L n
-- Mathlib.Data.ENat.Defs
ENat.recTopCoe_top : ∀ {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a), ENat.recTopCoe d f ⊤ = d
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent_C_mul_eq : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (f : Polynomial R),
  Polynomial.toLaurent (Polynomial.C r * f) = LaurentPolynomial.C r * Polynomial.toLaurent f
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.eq_iff : ∀ {K : Type u_1} [inst : Field K] {x y : NumberField.RingOfIntegers K}, ↑x = ↑y ↔ x = y
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.trans : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x y z : RingCat.Colimits.Prequotient F) (x_1 : RingCat.Colimits.Relation F x y)
  (x_2 : RingCat.Colimits.Relation F y z),
  RingCat.Colimits.Relation.below x_1 →
    motive x y x_1 → RingCat.Colimits.Relation.below x_2 → motive y z x_2 → RingCat.Colimits.Relation.below ⋯
-- Mathlib.Algebra.Free
FreeMagma.toFreeSemigroup_comp_of : ∀ {α : Type u}, ⇑FreeMagma.toFreeSemigroup ∘ FreeMagma.of = FreeSemigroup.of
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.instCompleteLattice : (ι : Type u_1) → CompleteLattice (PreAbstractSimplicialComplex ι)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Entrypoint.mk.injEq : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (aig : Std.Sat.AIG α) (ref : aig.Ref) (aig_1 : Std.Sat.AIG α)
  (ref_1 : aig_1.Ref), ({ aig := aig, ref := ref } = { aig := aig_1, ref := ref_1 }) = (aig = aig_1 ∧ ref ≍ ref_1)
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobeniusPoly.eq_1 : ∀ (p n : ℕ), WittVector.frobeniusPoly p n = MvPolynomial.X n ^ p + MvPolynomial.C ↑p * WittVector.frobeniusPolyAux p n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation P → P 2 = 0 → Q 2 ≠ 0 → W'.add P Q = (P 0 * Q 2) • Q
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.Saturate.below : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {K : CategoryTheory.Coverage C} →
      {motive : (X : C) → (a : CategoryTheory.Sieve X) → K.Saturate X a → Prop} →
        {X : C} → {a : CategoryTheory.Sieve X} → K.Saturate X a → Prop
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instAddMonoidWithOne : {R : Type u_1} → [AddMonoidWithOne R] → AddMonoidWithOne Rᵒᵈ
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃)
  (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X_1 : C₁) {X_2 Y : C₂}
  (f : X_2 ⟶ Y) (X_3 : C₃),
  (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).obj X_1).map f).app X_3 =
    ((X.obj (F₁.obj X_1)).map (F₂.map f)).app (F₃.obj X_3)
-- Mathlib.SetTheory.ZFC.Ordinal
/-- The union of transitive sets is transitive.  -/
ZFSet.IsTransitive.sUnion' : ∀ {x : ZFSet.{u}}, (∀ y ∈ x, y.IsTransitive) → x.sUnion.IsTransitive
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le' : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) {r r' : ℤ} (hrr' : r + 1 = r')
  (hr : r₀ ≤ r) (pq' : κ) {i₀' i₀ : ι}, i₀' = data.i₀ r' pq' ⋯ → i₀ = data.i₀ r pq' ⋯ → i₀' ≤ i₀
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- Quotienting `P^i / P^e` by its subspace `P^(i+1) ⧸ P^e` is
`R ⧸ p`-linearly isomorphic to `S ⧸ P`.  -/
Ideal.quotientRangePowQuotSuccInclusionEquiv : {R : Type u} →
  [inst : CommRing R] →
    {S : Type v} →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : Ideal R) →
            (P : Ideal S) →
              [hfp : NeZero (p.ramificationIdx' P)] →
                [IsDedekindDomain S] →
                  [P.IsPrime] →
                    P ≠ ⊥ →
                      {i : ℕ} →
                        i < p.ramificationIdx' P →
                          (↥(Ideal.map (Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (P ^ i)) ⧸
                              (p.powQuotSuccInclusion P i).range) ≃ₗ[R ⧸ p]
                            S ⧸ P
-- Mathlib.Data.Nat.Init
Nat.AtLeastTwo.toNeZero : ∀ (n : ℕ) [n.AtLeastTwo], NeZero n
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasure.measureOf_eq_coe : ∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α), m.measureOf = ⇑m
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.mem_support_iff_exists_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v}, w ∈ p.support ↔ w = v ∨ ∃ e ∈ p.edges, w ∈ e
-- Init.Data.List.Lemmas
List.head_eq_getLast_reverse : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.head h = l.reverse.getLast ⋯
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_one_iff' : ∀ {x y : ℝ}, 0 ≤ x → 0 < y → (x ^ y < 1 ↔ x < 1)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_div_left : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Div α] [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] (s t : Finset α) (f : α → β), (s / t).sup f = s.sup fun x => t.sup fun x_1 => f (x / x_1)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.instPreservesZeroMorphismsHomologyFunctor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C],
  (HomologicalComplex.homologyFunctor C c i).PreservesZeroMorphisms
-- Std.Data.Iterators.Producers.Range
/-- Returns an iterator over the given range. This iterator will emit the elements of the range
in increasing order.
 -/
Std.Rii.iter : {α : Type u_1} → [Std.PRange.Least? α] → Std.Rii α → Std.Iter α
-- Mathlib.Algebra.Ring.Subsemiring.Defs
SubsemiringClass.subtype_injective : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : SetLike S R] [hSR : SubsemiringClass S R] (s : S),
  Function.Injective ⇑(SubsemiringClass.subtype s)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.freeHomEquiv_symm_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} {I : Type u} (s : I → M.sections)
  (p : M ⟶ N),
  CategoryTheory.CategoryStruct.comp (M.freeHomEquiv.symm s) p =
    N.freeHomEquiv.symm fun i => SheafOfModules.sectionsMap p (s i)
-- Mathlib.Data.EReal.Basic
EReal.toReal_pos : ∀ {x : EReal}, 0 < x → x ≠ ⊤ → 0 < x.toReal
-- Mathlib.Computability.Reduce
ManyOneDegree.instPartialOrder : PartialOrder ManyOneDegree
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensor_left_unitality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)).hom h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X₁ X₂)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).hom
            (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₂).hom)
          h))
-- Lean.Elab.Tactic.Simp
Lean.Meta.Simp.ConfigWithOptions.mk.sizeOf_spec : ∀ (config : Lean.Meta.Simp.Config) (userConfig : Lean.Options),
  sizeOf { config := config, userConfig := userConfig } = 1 + sizeOf config + sizeOf userConfig
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_self : ∀ {a : ℤ}, a ≠ 0 → a.tdiv a = 1
-- Mathlib.Algebra.Notation.Indicator
/-- If an additive indicator function is not equal to `0` at a point, then that point is in the set.
 -/
Set.mem_of_indicator_ne_zero : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M} {a : α}, s.indicator f a ≠ 0 → a ∈ s
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.squareToSnd_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {i : CategoryTheory.Arrow C} {f : X ⟶ Y}
  {g : Y ⟶ Z} (sq : i ⟶ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp f g)),
  (CategoryTheory.Arrow.squareToSnd sq).left = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) f
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasStrictFDerivAt.finsetProd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {u : Finset ι} {g : ι → E → 𝔸'} {g' : ι → E →L[𝕜] 𝔸'} [inst_5 : DecidableEq ι] {x : E},
  (∀ i ∈ u, HasStrictFDerivAt (g i) (g' i) x) →
    HasStrictFDerivAt (fun x => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {fallback : β},
  Std.ExtDHashMap.Const.getD (m.erase k) a fallback =
    if (k == a) = true then fallback else Std.ExtDHashMap.Const.getD m a fallback
-- Mathlib.Order.BooleanAlgebra.Basic
le_sdiff_right : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x ≤ y \ x ↔ x = ⊥
-- Lean.Server.ServerTask
Lean.Server.ServerTask.pure : {α : Type u_1} → α → Lean.Server.ServerTask α
-- Mathlib.Data.Fintype.List
/-- Given a `m : Multiset α`, we form the `Multiset` of `l : List α` with the property `⟦l⟧ = m`.  -/
Multiset.lists : {α : Type u_1} → Multiset α → Multiset (List α)
-- Mathlib.Topology.ContinuousMap.StarOrdered
/-- A type class encoding the property that there is a continuous square root function on
nonnegative elements. This holds for `ℝ≥0`, `ℝ` and `ℂ` (as well as any C⋆-algebra), and this
allows us to derive an instance of `StarOrderedRing C(α, R)` under appropriate hypotheses.
In order for this to work on `ℝ≥0`, we actually must force our square root function to be defined
on and well-behaved for pairs `x : R × R` with `x.1 ≤ x.2`.  -/
ContinuousSqrt : (R : Type u_1) → [LE R] → [NonUnitalSemiring R] → [TopologicalSpace R] → Type u_1
-- Mathlib.Topology.Algebra.Group.Basic
nhds_translation_div : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] (x : G),
  Filter.comap (fun x_1 => x_1 / x) (nhds 1) = nhds x
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_cos_ofReal_re : ∀ (x : ℝ), ↑(Complex.cos ↑x).re = Complex.cos ↑x
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.xgcd.eq_1 : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (x y : R),
  EuclideanDomain.xgcd x y = (EuclideanDomain.xgcdAux x 1 0 y 0 1).2
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.mk_coordChange : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e₁ e₂ : Bundle.Trivialization F proj) {b : B},
  b ∈ e₁.baseSet → b ∈ e₂.baseSet → ∀ (x : F), (b, e₁.coordChange e₂ b x) = ↑e₂ (↑e₁.symm (b, x))
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitInclusiveIterator.instIteratorId.match_3.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice} (motive : Std.IterM Id String.Slice → Sort u_1) (currPos : s.Pos)
  (searcher : Std.Iter (String.Slice.Pattern.SearchStep s))
  (h_1 :
    (currPos : s.Pos) →
      (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive { internalState := String.Slice.SplitInclusiveIterator.operating currPos searcher })
  (h_2 : Unit → motive { internalState := String.Slice.SplitInclusiveIterator.atEnd }),
  (match { internalState := String.Slice.SplitInclusiveIterator.operating currPos searcher } with
    | { internalState := String.Slice.SplitInclusiveIterator.operating currPos searcher } => h_1 currPos searcher
    | { internalState := String.Slice.SplitInclusiveIterator.atEnd } => h_2 ()) =
    h_1 currPos searcher
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.inter_ground_subset_closure : ∀ {α : Type u_2} (M : Matroid α) (X : Set α), X ∩ M.E ⊆ M.closure X
-- Mathlib.Algebra.Notation
/-- The *positive part* of an element `a`.  -/
PosPart.posPart : {α : Type u_1} → [self : PosPart α] → α → α
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getUInt8Value? : Lean.Expr → OptionT Id UInt8
-- Mathlib.Algebra.Ring.Parity
Nat.Even.sub_odd : ∀ {m n : ℕ}, n ≤ m → Even m → Odd n → Odd (m - n)
-- Lean.Meta.Eqns
/-- Stores in the `eqnsExt` environment extension that `eqThms` are the equational theorems for `declName`
 -/
_private.Lean.Meta.Eqns.0.Lean.Meta.registerEqnThms : Lean.Name → Array Lean.Name → Lean.CoreM Unit
-- Mathlib.Data.Finite.Prod
Set.finite_image_fst_and_snd_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set (α × β)}, (Prod.fst '' s).Finite ∧ (Prod.snd '' s).Finite ↔ s.Finite