mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
/-- Suppose a function to angles is continuous on a connected set and never takes the values `0`
or `π` on that set. Then the values of the function on that set all have the same sign.  -/
Real.Angle.sign_eq_of_continuousOn : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → Real.Angle} {s : Set α} {x y : α},
  IsConnected s → ContinuousOn f s → (∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑Real.pi) → x ∈ s → y ∈ s → (f y).sign = (f x).sign
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.expand_one : ∀ {R : Type u_2} [inst : CommRing R], PowerSeries.expand 1 ⋯ = AlgHom.id R (PowerSeries R)
-- Mathlib.Topology.Order
nontrivialTopology_iff : ∀ (α : Type u_2) [inst : TopologicalSpace α], NontrivialTopology α ↔ inst ≠ ⊤
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_string : ∀ {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {s : String} {init : β} {f : Char → β → m (ForInStep β)}
  (inv : Std.Internal.Do.StringInvariant s β Pred) {epost : EPred},
  (∀ (pos : s.Pos) (b : β) (h : pos ≠ s.endPos),
      ⦃ inv pos b ⦄ f (pos.get h) b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv (pos.next h) b'
        | ForInStep.done b' => inv s.endPos b';
        epost ⦄) →
    ⦃ inv s.startPos init ⦄ forIn s init f ⦃ fun b => inv s.endPos b; epost ⦄
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.getInteractiveTermGoal : Lean.Lsp.PlainTermGoalParams → Lean.Server.RequestM (Lean.Server.RequestTask (Option Lean.Widget.InteractiveTermGoal))
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- A subset closed under the scalar action inherits that action.  -/
SetLike.smul : {S : Type u'} →
  {R : Type u} →
    {M : Type v} → [inst : SMul R M] → [inst_1 : SetLike S M] → [hS : SMulMemClass S R M] → (s : S) → SMul R ↥s
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebraClass.subtype_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Star A]
  [inst_3 : Module R A] {S : Type w''} [inst_4 : SetLike S A] [inst_5 : NonUnitalSubsemiringClass S A]
  [hSR : SMulMemClass S R A] [inst_6 : StarMemClass S A] {s : S} (x : ↥s),
  (NonUnitalStarSubalgebraClass.subtype s) x = ↑x
-- Init.Data.UInt.Lemmas
USize.ofBitVec_mod : ∀ (a b : BitVec System.Platform.numBits), { toBitVec := a % b } = { toBitVec := a } % { toBitVec := b }
-- Lean.Exception
/-- Throw an unknown identifier error message that is tagged with `unknownIdentifierMessageTag`.
The end position of the range of `ref` should always point at the unknown identifier.
See also `mkUnknownIdentifierMessage`.
 -/
Lean.throwUnknownIdentifierAt : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [Lean.MonadEnv m] →
        [Lean.MonadError m] → Lean.Syntax → Lean.MessageData → optParam Lean.Name Lean.Name.anonymous → m α
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.SimpAnd.mk : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs} {PQ : outParam (Std.Do.SPred σs)},
  (P ∧ Q ⊣⊢ₛ PQ) → Std.Do.SPred.Tactic.SimpAnd P Q PQ
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} → [inst : Max α] → [inst_1 : Bot α] → [inst_2 : Max β] → [inst_3 : Bot β] → FunLike (SupBotHom α β) α β
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_eq_one_of_card_eq_zero : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {A : Matrix n n R},
  Fintype.card n = 0 → A.det = 1
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.CancelParams.mk : Lean.JsonRpc.RequestID → Lean.Lsp.CancelParams
-- Mathlib.Data.Finset.Lattice.Basic
Finset.sup_eq_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊔ t = s ∪ t
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_1_comp_chainsIso₁ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  CategoryTheory.CategoryStruct.comp ((groupHomology.chainsMap f φ).f 1) (groupHomology.chainsIso₁ B).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₁ A).hom (groupHomology.chainsMap₁ f φ)
-- Mathlib.Tactic.Choose
/-- * `choose a b h h' using hyp` takes a hypothesis `hyp` of the form
  `∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b ∧ Q x y a b`
  for some `P Q : X → Y → A → B → Prop` and outputs
  into context a function `a : X → Y → A`, `b : X → Y → B` and two assumptions:
  `h : ∀ (x : X) (y : Y), P x y (a x y) (b x y)` and
  `h' : ∀ (x : X) (y : Y), Q x y (a x y) (b x y)`. It also works with dependent versions.

* `choose! a b h h' using hyp` does the same, except that it will remove dependency of
  the functions on propositional arguments if possible. For example if `Y` is a proposition
  and `A` and `B` are nonempty in the above example then we will instead get
  `a : X → A`, `b : X → B`, and the assumptions
  `h : ∀ (x : X) (y : Y), P x y (a x) (b x)` and
  `h' : ∀ (x : X) (y : Y), Q x y (a x) (b x)`.

The `using hyp` part can be omitted,
which will effectively cause `choose` to start with an `intro hyp`.

Like `intro`, the `choose` tactic supports type annotations to specify the expected type
of the introduced variables. This is useful for documentation and for catching mistakes early:
```
example (h : ∃ n : ℕ, n > 0) : True := by
  choose (n : ℕ) (hn : n > 0) using h
  trivial
```
If the provided type does not match the actual type, an error is raised.

Examples:

```
example (h : ∀ n m : ℕ, ∃ i j, m = n + i ∨ m + j = n) : True := by
  choose i j h using h
  guard_hyp i : ℕ → ℕ → ℕ
  guard_hyp j : ℕ → ℕ → ℕ
  guard_hyp h : ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n
  trivial
```

```
example (h : ∀ i : ℕ, i < 7 → ∃ j, i < j ∧ j < i+i) : True := by
  choose! f h h' using h
  guard_hyp f : ℕ → ℕ
  guard_hyp h : ∀ (i : ℕ), i < 7 → i < f i
  guard_hyp h' : ∀ (i : ℕ), i < 7 → f i < i + i
  trivial
```
 -/
Mathlib.Tactic.Choose.tacticChoose!___Using_ : Lean.ParserDescr
-- Mathlib.Order.BoundedOrder.Lattice
top_sup_eq : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] (a : α), ⊤ ⊔ a = ⊤
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.brecOn.go : {motive_1 : Lean.Lsp.DocumentSymbol → Sort u} →
  {motive_2 : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol → Sort u} →
    {motive_3 : Option (Array Lean.Lsp.DocumentSymbol) → Sort u} →
      {motive_4 : Array Lean.Lsp.DocumentSymbol → Sort u} →
        {motive_5 : List Lean.Lsp.DocumentSymbol → Sort u} →
          (t : Lean.Lsp.DocumentSymbol) →
            ((t : Lean.Lsp.DocumentSymbol) → t.below → motive_1 t) →
              ((t : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol) →
                  Lean.Lsp.DocumentSymbol.below_1 t → motive_2 t) →
                ((t : Option (Array Lean.Lsp.DocumentSymbol)) → Lean.Lsp.DocumentSymbol.below_2 t → motive_3 t) →
                  ((t : Array Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_3 t → motive_4 t) →
                    ((t : List Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_4 t → motive_5 t) →
                      motive_1 t ×' t.below
-- Mathlib.FieldTheory.Finite.Extension
Irreducible.natDegree_dvd_of_dvd_X_pow_card_pow_sub_X : ∀ {k : Type u_1} [inst : Field k] {f : Polynomial k},
  Irreducible f → ∀ {n : ℕ}, f ∣ Polynomial.X ^ Nat.card k ^ n - Polynomial.X → f.natDegree ∣ n
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_sSup : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Set (Subring Rᵐᵒᵖ)), (sSup S).unop = sSup (Subring.op ⁻¹' S)
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `FunLike.intCast_eq_zsmul_one`. -/
FunLike.coe_intCast : ∀ {F' : Type u_4} {α : Type u_5} [inst : FunLike F' α α] [inst_1 : IntCast F'] [inst_2 : One F'] [inst_3 : SMul ℤ α]
  [inst_4 : SMul ℤ F'] [IsSMulApply ℤ F' α α] [IsIntCastApply F' α] [IsOneApplyEqSelf F' α] (n : ℤ), ↑n = n • 1
-- Mathlib.Order.Defs.Unbundled
instSymmNe_mathlib : ∀ (α : Sort u_1), Std.Symm Ne
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.Augmented.σ₀Iter_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (Y : CategoryTheory.SimplicialObject.Augmented C)
  {n m : ℕ} (i : ℕ) (hi : autoParam (n + i = m) CategoryTheory.SimplicialObject.Augmented.σ₀Iter_hom_app._auto_1),
  CategoryTheory.CategoryStruct.comp (Y.left.σ₀Iter i hi) (Y.hom.app (Opposite.op { len := m })) =
    Y.hom.app (Opposite.op { len := n })
-- Std.Internal.Parsec.Basic
/-- Indicates that the parser reached the end of the input unexpectedly.
 -/
Std.Internal.Parsec.Error.eof : Std.Internal.Parsec.Error
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- The subscheme associated to an ideal sheaf `I` is covered by `Spec(Γ(X, U)/I(U))`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover : {X : AlgebraicGeometry.Scheme} → (I : X.IdealSheafData) → I.subscheme.AffineOpenCover
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_mul_iff_left : ∀ {R : Type u_1} [inst : CommRing R] {f g : Polynomial R} [IsDomain R], g ≠ 0 → g.Splits → ((f * g).Splits ↔ f.Splits)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.UnitLike.State.mk.inj : ∀ {map map_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr)}, { map := map } = { map := map_1 } → map = map_1
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_filterMapM_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : γ → o (Option δ)}
  {it : Std.IterM m β},
  (Std.IterM.filterMapM g (Std.IterM.filterMapWithPostcondition f it)).toList =
    (Std.IterM.filterMapM
        (fun b => do
          let __do_lift ← liftM (f b).run
          match __do_lift with
            | none => pure none
            | some fb => g fb)
        it).toList
-- Mathlib.Data.Fin.Fin2
/-- Converts a `Fin2` into a `Fin`.  -/
Fin2.toFin : {n : ℕ} → Fin2 n → Fin n
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instFaithfulForget : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.Grp.forget C).Faithful
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- `P` is local at the source if
1. `P` respects isomorphisms.
2. If `P` holds for `f : X ⟶ Y`, then `P` holds for `U.ι ≫ f` for any `U`.
3. If `P` holds for `U.ι ≫ f` for an open cover `U` of `X`, then `P` holds for `f`.
 -/
AlgebraicGeometry.IsZariskiLocalAtSource.mk' : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso],
  (∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (CategoryTheory.CategoryStruct.comp U.ι f)) →
    (∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens),
        iSup U = ⊤ → (∀ (i : ι), P (CategoryTheory.CategoryStruct.comp (U i).ι f)) → P f) →
      AlgebraicGeometry.IsZariskiLocalAtSource P
-- Mathlib.CategoryTheory.Opposites
Quiver.Hom.op_unop : ∀ {C : Type u₁} [inst : Quiver C] {X Y : Cᵒᵖ} (f : X ⟶ Y), f.unop.op = f
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.subLeft.eq_1 : ∀ {G : Type u_5} [inst : AddGroup G] (a : G),
  Equiv.subLeft a = { toFun := fun b => a - b, invFun := fun b => -b + a, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.ofHom_apply : ∀ {R : Type u} [inst : Semiring R] {M N : Type v} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] (f : M →ₗ[R] N) (x : M),
  (CategoryTheory.ConcreteCategory.hom (SemimoduleCat.ofHom f)) x = f x
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.precomp_obj_hom_app : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [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} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor C' C)
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L))
  (X_1 : C'), ((CategoryTheory.Functor.LeftExtension.precomp L F G).obj X).hom.app X_1 = X.hom.app (G.obj X_1)
-- Std.Http.Protocol.H1
/-- Whether this chunk finishes the current body stream.
 -/
Std.Http.Protocol.H1.PulledChunk.final : Std.Http.Protocol.H1.PulledChunk → Bool
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp.inj : ∀ {p : ENNReal} {V : Type u_1} {ofLp ofLp_1 : V}, WithLp.toLp p ofLp = WithLp.toLp p ofLp_1 → ofLp = ofLp_1
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
/-- Pull a subsemiring back to an opposite subsemiring along `MulOpposite.unop`  -/
Subsemiring.op : {R : Type u_2} → [inst : NonAssocSemiring R] → Subsemiring R → Subsemiring Rᵐᵒᵖ
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.id : ∀ {R : Type u_1} {ΓR : Type u_3} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero ΓR]
  (vR : Valuation R ΓR), vR.HasExtension vR
-- Mathlib.Data.Bool.Basic
Bool.toNat_bne_zero : ∀ (b : Bool), (b.toNat != 0) = b
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.instIsEquivalenceOppositeFiniteEtaleFintypeCatFiniteSpecOfIsSepClosed : ∀ (Ω : Type u) [inst : Field Ω] [IsSepClosed Ω], (CommAlgCat.FiniteEtale.finiteSpec Ω).IsEquivalence
-- Mathlib.LinearAlgebra.AffineSpace.Restrict
AffineMap.restrict.linear : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : AffineSubspace k P₁}
  {F : AffineSubspace k P₂} [inst_7 : Nonempty ↥E] [inst_8 : Nonempty ↥F] (hEF : AffineSubspace.map φ E ≤ F),
  (φ.restrict hEF).linear = φ.linear.restrict ⋯
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_eq_get_getKey? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : a ∈ m}, m.getKey a h = (m.getKey? a).get ⋯
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_union_distrib_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.continuous : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), Continuous ⇑e
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.ext : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  {v₁ v₂ : AddValuation R Γ₀}, (∀ (r : R), v₁ r = v₂ r) → v₁ = v₂
-- Mathlib.Data.WSeq.Basic
/-- The empty weak sequence  -/
Stream'.WSeq.nil : {α : Type u} → Stream'.WSeq α
-- Batteries.Data.String.Legacy
/-- Checks whether a substring contains the specified character.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.
 -/
Substring.Raw.Legacy.contains : Substring.Raw → Char → Bool
-- Mathlib.LinearAlgebra.Ray
exists_nonneg_right_iff_sameRay : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x y : M}, y ≠ 0 → ((∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R x y)
-- Mathlib.Tactic.Linter.Style
/-- `isCDot? stx` checks whether `stx` is a `Syntax` node corresponding to a `cdot` typed with
the character `·`.  -/
Mathlib.Linter.isCDot? : Lean.Syntax → Bool
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt.0.UInt32.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option UInt32)
-- Init.Data.Order.PackageFactories
Std.LinearOrderPackage.toLawfulOrderMax : ∀ {α : Type u} [self : Std.LinearOrderPackage α], Std.LawfulOrderMax α
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- The adjunction between `Over.map f` and `pullback f`.  -/
CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {Y X : C} →
      (f : Y ⟶ X) →
        [self : CategoryTheory.ChosenPullbacksAlong f] →
          CategoryTheory.Over.map f ⊣ CategoryTheory.ChosenPullbacksAlong.pullback f
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) {Z : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) A}
  (h : Φ₁.presheafFiber ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber f) h)
-- Mathlib.Topology.Algebra.AsymptoticCone
AffineSpace.asymptoticNhds.eq_1 : ∀ (k : Type u_1) {V : Type u_2} (P : Type u_3) [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] (v : V),
  AffineSpace.asymptoticNhds k P v = ⨆ p, Filter.atTop • nhds v +ᵥ pure p
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_add : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  (x y : R), min (v x) (v y) ≤ v (x + y)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- The continuous functional calculus commutes with integration.
For a version with stronger assumptions which in practice are often easier to verify, see
`cfcₙ_integral`.  -/
cfcₙ_integral' : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NonUnitalNormedRing A] [inst_3 : StarRing A] [inst_4 : NormedSpace 𝕜 A]
  [inst_5 : IsScalarTower 𝕜 A A] [inst_6 : SMulCommClass 𝕜 A A] [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p]
  [inst_8 : CompleteSpace A] [inst_9 : NormedSpace ℝ A] (f : X → 𝕜 → 𝕜) (a : A),
  (∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)) →
    (∀ᵐ (x : X) ∂μ, f x 0 = 0) →
      MeasureTheory.Integrable (fun x => ContinuousMapZero.mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ →
        autoParam (p a) cfcₙ_integral'._auto_1 → cfcₙ (fun z => ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfcₙ (f x) a ∂μ
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.coeff_mapAddEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Add M] (e : R ≃+ S)
  (x : AddMonoidAlgebra R M) (m : M), ((AddMonoidAlgebra.mapAddEquiv M e) x).coeff m = e (x.coeff m)
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_univ_left : ∀ {G : Type u_1} [inst : AddGroup G] {S : Set G}, AddSubgroup.IsComplement Set.univ S ↔ ∃ g, S = {g}
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zmodEquivZPowers.congr_simp : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k), h.zmodEquivZPowers = h.zmodEquivZPowers
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise scalar multiplication of `f` and
`g`, which monovary together on `s`, is unchanged by a permutation if and only if `f` and `g ∘ σ`
monovary together on `s`. Stated by permuting the entries of `g`.  -/
MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
  MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i ↔ MonovaryOn f (g ∘ ⇑σ) ↑s)
-- Std.Time.Format.Modifier
Std.Time.Modifier.X.sizeOf_spec : ∀ (presentation : Std.Time.OffsetX), sizeOf (Std.Time.Modifier.X presentation) = 1 + sizeOf presentation
-- Mathlib.Order.Hom.BoundedLattice
/-- The function preserves the top element. The preferred spelling is `map_top`.  -/
InfTopHom.map_top' : ∀ {α : Type u_6} {β : Type u_7} [inst : Min α] [inst_1 : Min β] [inst_2 : Top α] [inst_3 : Top β]
  (self : InfTopHom α β), self.toFun ⊤ = ⊤
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map_H0Iso_hom_f_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k}
  (h : (groupCohomology.shortComplexH0 B).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.map f φ 0)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso B).hom
        (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH0 B).f h)) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH0 A).f
        (CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom φ) h))
-- Mathlib.Algebra.AddConstMap.Equiv
/-- Projection from `G ≃+c[a, a] G` to `G →+c[a, a] G`, as a monoid homomorphism.  -/
AddConstEquiv.toAddConstMapHom : {G : Type u_1} → [inst : Add G] → {a : G} → AddConstEquiv G G a a →* AddConstMap G G a a
-- Mathlib.CategoryTheory.ObjectProperty.Local
CategoryTheory.MorphismProperty.instIsClosedUnderLimitsOfShapeIsLocal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], W.isLocal.IsClosedUnderLimitsOfShape J
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.ofIsoComp_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X)
  [inst_1 : CategoryTheory.IsIso g]
  (F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g f)),
  (CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F).I = F.I
-- Lean.Parser.Term
Lean.Parser.Term.withAnonymousAntiquot : Lean.Parser.Parser
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftFunction.lift_seqRight : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] {lift : ⦃α : Type u⦄ → m α → n α}
  {α β : Type u} [LawfulMonad m] [LawfulMonad n] [Std.Internal.LawfulMonadLiftFunction lift] (x : m α) (y : m β),
  lift (x *> y) = lift x *> lift y
-- Mathlib.Topology.Algebra.UniformConvergence
instOneUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : One β],
  instOneUniformOnFun = { one := instOneUniformOnFun._aux_1 }